Metamath Proof Explorer

Theorem sn-axprlem3

Description: axprlem3 using only Tarski's FOL axiom schemes and ax-rep . (Contributed by SN, 22-Sep-2023)

Ref Expression
Assertion sn-axprlem3 
|- E. y A. z ( z e. y <-> E. w e. x if- ( ph , z = a , z = b ) )

Proof

Step Hyp Ref Expression
1 axrep6 
 |-  ( A. w E* z if- ( ph , z = a , z = b ) -> E. y A. z ( z e. y <-> E. w e. x if- ( ph , z = a , z = b ) ) )
2 ax6evr 
 |-  E. y a = y
3 ifptru 
 |-  ( ph -> ( if- ( ph , z = a , z = b ) <-> z = a ) )
4 3 biimpd 
 |-  ( ph -> ( if- ( ph , z = a , z = b ) -> z = a ) )
5 equtrr 
 |-  ( a = y -> ( z = a -> z = y ) )
6 4 5 sylan9r 
 |-  ( ( a = y /\ ph ) -> ( if- ( ph , z = a , z = b ) -> z = y ) )
7 6 alrimiv 
 |-  ( ( a = y /\ ph ) -> A. z ( if- ( ph , z = a , z = b ) -> z = y ) )
8 7 expcom 
 |-  ( ph -> ( a = y -> A. z ( if- ( ph , z = a , z = b ) -> z = y ) ) )
9 8 eximdv 
 |-  ( ph -> ( E. y a = y -> E. y A. z ( if- ( ph , z = a , z = b ) -> z = y ) ) )
10 2 9 mpi 
 |-  ( ph -> E. y A. z ( if- ( ph , z = a , z = b ) -> z = y ) )
11 ax6evr 
 |-  E. y b = y
12 ifpfal 
 |-  ( -. ph -> ( if- ( ph , z = a , z = b ) <-> z = b ) )
13 12 biimpd 
 |-  ( -. ph -> ( if- ( ph , z = a , z = b ) -> z = b ) )
14 equtrr 
 |-  ( b = y -> ( z = b -> z = y ) )
15 13 14 sylan9r 
 |-  ( ( b = y /\ -. ph ) -> ( if- ( ph , z = a , z = b ) -> z = y ) )
16 15 alrimiv 
 |-  ( ( b = y /\ -. ph ) -> A. z ( if- ( ph , z = a , z = b ) -> z = y ) )
17 16 expcom 
 |-  ( -. ph -> ( b = y -> A. z ( if- ( ph , z = a , z = b ) -> z = y ) ) )
18 17 eximdv 
 |-  ( -. ph -> ( E. y b = y -> E. y A. z ( if- ( ph , z = a , z = b ) -> z = y ) ) )
19 11 18 mpi 
 |-  ( -. ph -> E. y A. z ( if- ( ph , z = a , z = b ) -> z = y ) )
20 10 19 pm2.61i 
 |-  E. y A. z ( if- ( ph , z = a , z = b ) -> z = y )
21 df-mo 
 |-  ( E* z if- ( ph , z = a , z = b ) <-> E. y A. z ( if- ( ph , z = a , z = b ) -> z = y ) )
22 20 21 mpbir 
 |-  E* z if- ( ph , z = a , z = b )
23 1 22 mpg 
 |-  E. y A. z ( z e. y <-> E. w e. x if- ( ph , z = a , z = b ) )