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 × D / R
3ecoptocl.2 x y R = A φ ψ
3ecoptocl.3 z w R = B ψ χ
3ecoptocl.4 v u R = C χ θ
3ecoptocl.5 x D y D z D w D v D u D φ
Assertion 3ecoptocl A S B S C S θ

Proof

Step Hyp Ref Expression
1 3ecoptocl.1 S = D × D / R
2 3ecoptocl.2 x y R = A φ ψ
3 3ecoptocl.3 z w R = B ψ χ
4 3ecoptocl.4 v u R = C χ θ
5 3ecoptocl.5 x D y D z D w D v D u D φ
6 3 imbi2d z w R = B A S ψ A S χ
7 4 imbi2d v u R = C A S χ A S θ
8 2 imbi2d x y R = A z D w D v D u D φ z D w D v D u D ψ
9 5 3expib x D y D z D w D v D u D φ
10 1 8 9 ecoptocl A S z D w D v D u D ψ
11 10 com12 z D w D v D u D A S ψ
12 1 6 7 11 2ecoptocl B S C S A S θ
13 12 com12 A S B S C S θ
14 13 3impib A S B S C S θ