Theorem exdistrf
Distribution of existential quantifiers, with a bound-variable
hypothesis saying that \( y \) is not free in \( \varphi \), but \( x \) can be
free in \( \varphi \) (and there is no distinct variable condition on \( x \) and
\( y \) ). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof
shortened by Wolf Lammen, 14-May-2018.) Usage of this theorem is
discouraged because it depends on [ax-13]. Use exdistr instead.
(New usage is discouraged.)
Hypothesis
exdistrf.1
\( \vdash \neg \forall x \, x = y \rightarrow \Finv y \, \varphi \)
Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \rightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
Proof
l0
nfe1
19.8a
anim2i _
l3
eximi _
\( \vdash \exists y \, (\varphi \wedge \psi) \rightarrow \exists y \, (\varphi \wedge \exists y \, \psi) \)
biidd
drex1 _
\( \vdash \forall x \, x = y \rightarrow (\exists x \, (\varphi \wedge \exists y \, \psi) \leftrightarrow \exists y \, (\varphi \wedge \exists y \, \psi)) \)
l6
imbitrrid l3 _
\( \vdash \forall x \, x = y \rightarrow \exists y \, (\varphi \wedge \psi) \rightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
l7
19.40
\( \vdash \exists y \, (\varphi \wedge \psi) \rightarrow \exists y \, \varphi \wedge \exists y \, \psi \)
exdistrf.1
19.9d _
l10
anim1d _
\( \vdash \neg \forall x \, x = y \rightarrow \exists y \, \varphi \wedge \exists y \, \psi \rightarrow \varphi \wedge \exists y \, \psi \)
19.8a
\( \vdash \varphi \wedge \exists y \, \psi \rightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
syl56 l7 l10 _
\( \vdash \neg \forall x \, x = y \rightarrow \exists y \, (\varphi \wedge \psi) \rightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
pm2.61i l6 _
exlimi l0 _