Theorem 2optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

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

Proof

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