Predicate Logic - Difference between two english translated predicate statements I translated the statement "If at least one python program is correct, then all python programs are correct." Given the predicates $Python(x)$, $Correct(x)$, and the set of all programs $p$.
I have:

$\exists x \in p, \forall y \in p, Python(x) \land Correct(x) \implies Python(y) \land Correct(y)$

However, the correct answer I was given/told was:

$(\exists x \in p, Python(x) \land Correct(x)) \implies (\forall y \in p, Python(y) \implies Correct(y))$

I can see why the second is 100% correct in capturing the original statements meaning, but I cannot see intuitively why my original statement does not. Anybody have a good way to explain the difference for future reference? The only thing I can think of is that my statement CAN be vacuously true when $x$ is not a python program and correct...
 A: Translating your formal statement back into English reads like this:

There exists a program such that if this program is a correct python program, then every program is a correct python program.

As you noticed yourself, this statement is trivially true if there exists a program which is not a python program or not correct. So, in particular, your statement is clearly true in our world, while the given statement clearly is not.
I want to note, however, that the "correct answer" seems to be wrong, too. Translating this statement back to English actually reads:

If at least one python program is correct, then all programs are correct python programs.

I would rather translate the given statement as follows:

$(\exists x \in p, Python(x) \land Correct(x)) \implies (\forall y \in p, Python(y) \implies Correct(y))$

A: 
$\exists x \in p, \forall y \in p, Python(x) \land Correct(x) \implies Python(y) \land Correct(y)$

As written, due to precedence conventions, your suggested sentence is technically is equivalent to $$\big(\exists x {\in} p \;\forall y {\in} p\; Px\big) \land Cx \implies Py \land Cy.$$
But I suppose you actually meant $$\exists x {\in} p \;\forall y {\in} p\; \big(Px \land Cx \implies Py \land Cy\big),\tag#$$ which is the Prenex form of (and thus equivalent to) $$\forall x {\in} p \;\big(Px \land Cx\big) \implies \forall y {\in} p\;\big( Py \land Cy\big),\tag#$$ which is clearly not equivalent to $$\exists x {\in} p \;\big(Px \land Cx\big) \implies \forall y {\in} p\;\big( Py \implies Cy\big),\tag✔$$ which is the correct answer.
$(\#)$ is actually a first-order tautology (logically true), can be rewritten as $$\forall x {\in} p \;\big(Px \land Cx\big) \implies \forall x {\in} p\;\big( Px \land Cx\big),$$ and is literally read as “if every program is Python and correct, then every program is Python and correct”.

However, the correct answer I was given/told was:
$(\exists x \in p, Python(x) \land Correct(x)) \implies (\forall y \in p, Python(y) \implies Correct(y))$

This answer is actually also not correct, as it is technically equivalent to $$\big((\exists x {\in} p\;Px) \land Cx\big) \implies \big((\forall y {\in} p\; Py) \implies Cy\big),$$ which is not equivalent to $(✔).$
