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

Metamath Proof Explorer

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 )