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

Metamath Proof Explorer

Theorem cgsexg

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

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

Proof

Step Hyp Ref Expression
1 cgsexg.1 
 |-  ( x = A -> ch )
2 cgsexg.2 
 |-  ( ch -> ( ph <-> ps ) )
3 2 biimpa 
 |-  ( ( ch /\ ph ) -> ps )
4 3 exlimiv 
 |-  ( E. x ( ch /\ ph ) -> ps )
5 elisset 
 |-  ( A e. V -> E. x x = A )
6 1 eximi 
 |-  ( E. x x = A -> E. x ch )
7 5 6 syl 
 |-  ( A e. V -> E. x ch )
8 2 biimprcd 
 |-  ( ps -> ( ch -> ph ) )
9 8 ancld 
 |-  ( ps -> ( ch -> ( ch /\ ph ) ) )
10 9 eximdv 
 |-  ( ps -> ( E. x ch -> E. x ( ch /\ ph ) ) )
11 7 10 syl5com 
 |-  ( A e. V -> ( ps -> E. x ( ch /\ ph ) ) )
12 4 11 impbid2 
 |-  ( A e. V -> ( E. x ( ch /\ ph ) <-> ps ) )