# 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}=\left({C}×{D}\right)/{R}$
2ecoptocl.2 ${⊢}\left[⟨{x},{y}⟩\right]{R}={A}\to \left({\phi }↔{\psi }\right)$
2ecoptocl.3 ${⊢}\left[⟨{z},{w}⟩\right]{R}={B}\to \left({\psi }↔{\chi }\right)$
2ecoptocl.4 ${⊢}\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\to {\phi }$
Assertion 2ecoptocl ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {\chi }$

### Proof

Step Hyp Ref Expression
1 2ecoptocl.1 ${⊢}{S}=\left({C}×{D}\right)/{R}$
2 2ecoptocl.2 ${⊢}\left[⟨{x},{y}⟩\right]{R}={A}\to \left({\phi }↔{\psi }\right)$
3 2ecoptocl.3 ${⊢}\left[⟨{z},{w}⟩\right]{R}={B}\to \left({\psi }↔{\chi }\right)$
4 2ecoptocl.4 ${⊢}\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\to {\phi }$
5 3 imbi2d ${⊢}\left[⟨{z},{w}⟩\right]{R}={B}\to \left(\left({A}\in {S}\to {\psi }\right)↔\left({A}\in {S}\to {\chi }\right)\right)$
6 2 imbi2d ${⊢}\left[⟨{x},{y}⟩\right]{R}={A}\to \left(\left(\left({z}\in {C}\wedge {w}\in {D}\right)\to {\phi }\right)↔\left(\left({z}\in {C}\wedge {w}\in {D}\right)\to {\psi }\right)\right)$
7 4 ex ${⊢}\left({x}\in {C}\wedge {y}\in {D}\right)\to \left(\left({z}\in {C}\wedge {w}\in {D}\right)\to {\phi }\right)$
8 1 6 7 ecoptocl ${⊢}{A}\in {S}\to \left(\left({z}\in {C}\wedge {w}\in {D}\right)\to {\psi }\right)$
9 8 com12 ${⊢}\left({z}\in {C}\wedge {w}\in {D}\right)\to \left({A}\in {S}\to {\psi }\right)$
10 1 5 9 ecoptocl ${⊢}{B}\in {S}\to \left({A}\in {S}\to {\chi }\right)$
11 10 impcom ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {\chi }$