Theorem exdistrf

Description: Distribution of existential quantifiers, with a bound-variable hypothesis saying that y is not free in ph , but x can be free in ph (and there is no distinct variable condition on x and y ). Usage of this theorem is discouraged because it depends on ax-13 . Check out exdistr for a version requiring fewer axioms. (Contributed by Mario Carneiro, 20-Mar-2013) (Proof shortened by Wolf Lammen, 14-May-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	exdistrf.1	|- ( -. A. x x = y -> F/ y ph )
Assertion	exdistrf	|- ( E. x E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrf.1	|- ( -. A. x x = y -> F/ y ph )
2		nfe1	|- F/ x E. x ( ph /\ E. y ps )
3		19.8a	|- ( ps -> E. y ps )
4	3	anim2i	|- ( ( ph /\ ps ) -> ( ph /\ E. y ps ) )
5	4	eximi	|- ( E. y ( ph /\ ps ) -> E. y ( ph /\ E. y ps ) )
6		biidd	|- ( A. x x = y -> ( ( ph /\ E. y ps ) <-> ( ph /\ E. y ps ) ) )
7	6	drex1	|- ( A. x x = y -> ( E. x ( ph /\ E. y ps ) <-> E. y ( ph /\ E. y ps ) ) )
8	5 7	syl5ibr	|- ( A. x x = y -> ( E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) ) )
9		19.40	|- ( E. y ( ph /\ ps ) -> ( E. y ph /\ E. y ps ) )
10	1	19.9d	|- ( -. A. x x = y -> ( E. y ph -> ph ) )
11	10	anim1d	|- ( -. A. x x = y -> ( ( E. y ph /\ E. y ps ) -> ( ph /\ E. y ps ) ) )
12		19.8a	|- ( ( ph /\ E. y ps ) -> E. x ( ph /\ E. y ps ) )
13	9 11 12	syl56	|- ( -. A. x x = y -> ( E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) ) )
14	8 13	pm2.61i	|- ( E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) )
15	2 14	exlimi	|- ( E. x E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) )