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

Metamath Proof Explorer

Theorem cgsex2g

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995)

Ref Expression
Hypotheses cgsex2g.1 
|- ( ( x = A /\ y = B ) -> ch )
cgsex2g.2 
|- ( ch -> ( ph <-> ps ) )
Assertion cgsex2g 
|- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ch /\ ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 cgsex2g.1 
 |-  ( ( x = A /\ y = B ) -> ch )
2 cgsex2g.2 
 |-  ( ch -> ( ph <-> ps ) )
3 2 biimpa 
 |-  ( ( ch /\ ph ) -> ps )
4 3 exlimivv 
 |-  ( E. x E. y ( ch /\ ph ) -> ps )
5 elisset 
 |-  ( A e. V -> E. x x = A )
6 elisset 
 |-  ( B e. W -> E. y y = B )
7 5 6 anim12i 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
8 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
9 7 8 sylibr 
 |-  ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
10 1 2eximi 
 |-  ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ch )
11 9 10 syl 
 |-  ( ( A e. V /\ B e. W ) -> E. x E. y ch )
12 2 biimprcd 
 |-  ( ps -> ( ch -> ph ) )
13 12 ancld 
 |-  ( ps -> ( ch -> ( ch /\ ph ) ) )
14 13 2eximdv 
 |-  ( ps -> ( E. x E. y ch -> E. x E. y ( ch /\ ph ) ) )
15 11 14 syl5com 
 |-  ( ( A e. V /\ B e. W ) -> ( ps -> E. x E. y ( ch /\ ph ) ) )
16 4 15 impbid2 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ch /\ ph ) <-> ps ) )