Metamath Proof Explorer

Theorem rexsb

Description: An equivalent expression for restricted existence, analogous to exsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion rexsb 
|- ( E. x e. A ph <-> E. y e. A A. x ( x = y -> ph ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ph
2 nfa1 
 |-  F/ x A. x ( x = y -> ph )
3 ax12v 
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
4 sp 
 |-  ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
5 4 com12 
 |-  ( x = y -> ( A. x ( x = y -> ph ) -> ph ) )
6 3 5 impbid 
 |-  ( x = y -> ( ph <-> A. x ( x = y -> ph ) ) )
7 1 2 6 cbvrexw 
 |-  ( E. x e. A ph <-> E. y e. A A. x ( x = y -> ph ) )