Metamath Proof Explorer

Theorem rexrsb

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

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

Proof

Step Hyp Ref Expression
1 rexsb 
 |-  ( E. x e. A ph <-> E. y e. A A. x ( x = y -> ph ) )
2 alral 
 |-  ( A. x ( x = y -> ph ) -> A. x e. A ( x = y -> ph ) )
3 df-ral 
 |-  ( A. x e. A ( x = y -> ph ) <-> A. x ( x e. A -> ( x = y -> ph ) ) )
4 19.27v 
 |-  ( A. x ( ( x e. A -> ( x = y -> ph ) ) /\ y e. A ) <-> ( A. x ( x e. A -> ( x = y -> ph ) ) /\ y e. A ) )
5 pm2.04 
 |-  ( ( x e. A -> ( x = y -> ph ) ) -> ( x = y -> ( x e. A -> ph ) ) )
6 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
7 6 biimprd 
 |-  ( x = y -> ( y e. A -> x e. A ) )
8 7 imim1d 
 |-  ( x = y -> ( ( x e. A -> ph ) -> ( y e. A -> ph ) ) )
9 8 a2i 
 |-  ( ( x = y -> ( x e. A -> ph ) ) -> ( x = y -> ( y e. A -> ph ) ) )
10 pm2.04 
 |-  ( ( x = y -> ( y e. A -> ph ) ) -> ( y e. A -> ( x = y -> ph ) ) )
11 5 9 10 3syl 
 |-  ( ( x e. A -> ( x = y -> ph ) ) -> ( y e. A -> ( x = y -> ph ) ) )
12 11 imp 
 |-  ( ( ( x e. A -> ( x = y -> ph ) ) /\ y e. A ) -> ( x = y -> ph ) )
13 12 alimi 
 |-  ( A. x ( ( x e. A -> ( x = y -> ph ) ) /\ y e. A ) -> A. x ( x = y -> ph ) )
14 4 13 sylbir 
 |-  ( ( A. x ( x e. A -> ( x = y -> ph ) ) /\ y e. A ) -> A. x ( x = y -> ph ) )
15 14 ex 
 |-  ( A. x ( x e. A -> ( x = y -> ph ) ) -> ( y e. A -> A. x ( x = y -> ph ) ) )
16 3 15 sylbi 
 |-  ( A. x e. A ( x = y -> ph ) -> ( y e. A -> A. x ( x = y -> ph ) ) )
17 16 com12 
 |-  ( y e. A -> ( A. x e. A ( x = y -> ph ) -> A. x ( x = y -> ph ) ) )
18 2 17 impbid2 
 |-  ( y e. A -> ( A. x ( x = y -> ph ) <-> A. x e. A ( x = y -> ph ) ) )
19 18 rexbiia 
 |-  ( E. y e. A A. x ( x = y -> ph ) <-> E. y e. A A. x e. A ( x = y -> ph ) )
20 1 19 bitri 
 |-  ( E. x e. A ph <-> E. y e. A A. x e. A ( x = y -> ph ) )