Metamath Proof Explorer

Theorem axunndlem1

Description: Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axunndlem1 
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )

Proof

Step Hyp Ref Expression
1 en2lp 
 |-  -. ( y e. x /\ x e. y )
2 elequ2 
 |-  ( y = z -> ( x e. y <-> x e. z ) )
3 2 anbi2d 
 |-  ( y = z -> ( ( y e. x /\ x e. y ) <-> ( y e. x /\ x e. z ) ) )
4 1 3 mtbii 
 |-  ( y = z -> -. ( y e. x /\ x e. z ) )
5 4 sps 
 |-  ( A. y y = z -> -. ( y e. x /\ x e. z ) )
6 5 nexdv 
 |-  ( A. y y = z -> -. E. x ( y e. x /\ x e. z ) )
7 6 pm2.21d 
 |-  ( A. y y = z -> ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
8 7 axc4i 
 |-  ( A. y y = z -> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
9 8 19.8ad 
 |-  ( A. y y = z -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
10 zfun 
 |-  E. x A. w ( E. x ( w e. x /\ x e. z ) -> w e. x )
11 nfnae 
 |-  F/ y -. A. y y = z
12 nfnae 
 |-  F/ x -. A. y y = z
13 nfvd 
 |-  ( -. A. y y = z -> F/ y w e. x )
14 nfcvf 
 |-  ( -. A. y y = z -> F/_ y z )
15 14 nfcrd 
 |-  ( -. A. y y = z -> F/ y x e. z )
16 13 15 nfand 
 |-  ( -. A. y y = z -> F/ y ( w e. x /\ x e. z ) )
17 12 16 nfexd 
 |-  ( -. A. y y = z -> F/ y E. x ( w e. x /\ x e. z ) )
18 17 13 nfimd 
 |-  ( -. A. y y = z -> F/ y ( E. x ( w e. x /\ x e. z ) -> w e. x ) )
19 elequ1 
 |-  ( w = y -> ( w e. x <-> y e. x ) )
20 19 anbi1d 
 |-  ( w = y -> ( ( w e. x /\ x e. z ) <-> ( y e. x /\ x e. z ) ) )
21 20 exbidv 
 |-  ( w = y -> ( E. x ( w e. x /\ x e. z ) <-> E. x ( y e. x /\ x e. z ) ) )
22 21 19 imbi12d 
 |-  ( w = y -> ( ( E. x ( w e. x /\ x e. z ) -> w e. x ) <-> ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
23 22 a1i 
 |-  ( -. A. y y = z -> ( w = y -> ( ( E. x ( w e. x /\ x e. z ) -> w e. x ) <-> ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) ) )
24 11 18 23 cbvald 
 |-  ( -. A. y y = z -> ( A. w ( E. x ( w e. x /\ x e. z ) -> w e. x ) <-> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
25 24 exbidv 
 |-  ( -. A. y y = z -> ( E. x A. w ( E. x ( w e. x /\ x e. z ) -> w e. x ) <-> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
26 10 25 mpbii 
 |-  ( -. A. y y = z -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
27 9 26 pm2.61i 
 |-  E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )