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

Metamath Proof Explorer

Theorem 2gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

Ref Expression
Hypotheses 2gencl.1 
|- ( C e. S <-> E. x e. R A = C )
2gencl.2 
|- ( D e. S <-> E. y e. R B = D )
2gencl.3 
|- ( A = C -> ( ph <-> ps ) )
2gencl.4 
|- ( B = D -> ( ps <-> ch ) )
2gencl.5 
|- ( ( x e. R /\ y e. R ) -> ph )
Assertion 2gencl 
|- ( ( C e. S /\ D e. S ) -> ch )

Proof

Step Hyp Ref Expression
1 2gencl.1 
 |-  ( C e. S <-> E. x e. R A = C )
2 2gencl.2 
 |-  ( D e. S <-> E. y e. R B = D )
3 2gencl.3 
 |-  ( A = C -> ( ph <-> ps ) )
4 2gencl.4 
 |-  ( B = D -> ( ps <-> ch ) )
5 2gencl.5 
 |-  ( ( x e. R /\ y e. R ) -> ph )
6 df-rex 
 |-  ( E. y e. R B = D <-> E. y ( y e. R /\ B = D ) )
7 2 6 bitri 
 |-  ( D e. S <-> E. y ( y e. R /\ B = D ) )
8 4 imbi2d 
 |-  ( B = D -> ( ( C e. S -> ps ) <-> ( C e. S -> ch ) ) )
9 df-rex 
 |-  ( E. x e. R A = C <-> E. x ( x e. R /\ A = C ) )
10 1 9 bitri 
 |-  ( C e. S <-> E. x ( x e. R /\ A = C ) )
11 3 imbi2d 
 |-  ( A = C -> ( ( y e. R -> ph ) <-> ( y e. R -> ps ) ) )
12 5 ex 
 |-  ( x e. R -> ( y e. R -> ph ) )
13 10 11 12 gencl 
 |-  ( C e. S -> ( y e. R -> ps ) )
14 13 com12 
 |-  ( y e. R -> ( C e. S -> ps ) )
15 7 8 14 gencl 
 |-  ( D e. S -> ( C e. S -> ch ) )
16 15 impcom 
 |-  ( ( C e. S /\ D e. S ) -> ch )