Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 2ecoptocl.1 S = C × D / R
2 2ecoptocl.2 x y R = A φ ψ
3 2ecoptocl.3 z w R = B ψ χ
4 2ecoptocl.4 x C y D z C w D φ
5 3 imbi2d z w R = B A S ψ A S χ
6 2 imbi2d x y R = A z C w D φ z C w D ψ
7 4 ex x C y D z C w D φ
8 1 6 7 ecoptocl A S z C w D ψ
9 8 com12 z C w D A S ψ
10 1 5 9 ecoptocl B S A S χ
11 10 impcom A S B S χ