This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ). (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.)

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 imbitrrid 
 |-  ( 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 ) )