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

Metamath Proof Explorer

Theorem 3ecoptocl

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

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

Proof

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