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 )