Theorem 2ecoptocl

Description: Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995)

	Ref	Expression
Hypotheses	2ecoptocl.1	|- S = ( ( C X. D ) /. R )
	2ecoptocl.2	|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
	2ecoptocl.3	|- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )
	2ecoptocl.4	|- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )
Assertion	2ecoptocl	|- ( ( A e. S /\ B e. S ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		2ecoptocl.1	|- S = ( ( C X. D ) /. R )
2		2ecoptocl.2	|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )
3		2ecoptocl.3	|- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )
4		2ecoptocl.4	|- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )
5	3	imbi2d	|- ( [ <. z , w >. ] R = B -> ( ( A e. S -> ps ) <-> ( A e. S -> ch ) ) )
6	2	imbi2d	|- ( [ <. x , y >. ] R = A -> ( ( ( z e. C /\ w e. D ) -> ph ) <-> ( ( z e. C /\ w e. D ) -> ps ) ) )
7	4	ex	|- ( ( x e. C /\ y e. D ) -> ( ( z e. C /\ w e. D ) -> ph ) )
8	1 6 7	ecoptocl	|- ( A e. S -> ( ( z e. C /\ w e. D ) -> ps ) )
9	8	com12	|- ( ( z e. C /\ w e. D ) -> ( A e. S -> ps ) )
10	1 5 9	ecoptocl	|- ( B e. S -> ( A e. S -> ch ) )
11	10	impcom	|- ( ( A e. S /\ B e. S ) -> ch )