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

### Proof

Step Hyp Ref Expression
1 2optocl.1 ${⊢}{R}={C}×{D}$
2 2optocl.2 ${⊢}⟨{x},{y}⟩={A}\to \left({\phi }↔{\psi }\right)$
3 2optocl.3 ${⊢}⟨{z},{w}⟩={B}\to \left({\psi }↔{\chi }\right)$
4 2optocl.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 ${⊢}⟨{z},{w}⟩={B}\to \left(\left({A}\in {R}\to {\psi }\right)↔\left({A}\in {R}\to {\chi }\right)\right)$
6 2 imbi2d ${⊢}⟨{x},{y}⟩={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 optocl ${⊢}{A}\in {R}\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 {R}\to {\psi }\right)$
10 1 5 9 optocl ${⊢}{B}\in {R}\to \left({A}\in {R}\to {\chi }\right)$
11 10 impcom ${⊢}\left({A}\in {R}\wedge {B}\in {R}\right)\to {\chi }$