# Metamath Proof Explorer

## Theorem 3optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

Ref Expression
Hypotheses 3optocl.1 ${⊢}{R}={D}×{F}$
3optocl.2 ${⊢}⟨{x},{y}⟩={A}\to \left({\phi }↔{\psi }\right)$
3optocl.3 ${⊢}⟨{z},{w}⟩={B}\to \left({\psi }↔{\chi }\right)$
3optocl.4 ${⊢}⟨{v},{u}⟩={C}\to \left({\chi }↔{\theta }\right)$
3optocl.5 ${⊢}\left(\left({x}\in {D}\wedge {y}\in {F}\right)\wedge \left({z}\in {D}\wedge {w}\in {F}\right)\wedge \left({v}\in {D}\wedge {u}\in {F}\right)\right)\to {\phi }$
Assertion 3optocl ${⊢}\left({A}\in {R}\wedge {B}\in {R}\wedge {C}\in {R}\right)\to {\theta }$

### Proof

Step Hyp Ref Expression
1 3optocl.1 ${⊢}{R}={D}×{F}$
2 3optocl.2 ${⊢}⟨{x},{y}⟩={A}\to \left({\phi }↔{\psi }\right)$
3 3optocl.3 ${⊢}⟨{z},{w}⟩={B}\to \left({\psi }↔{\chi }\right)$
4 3optocl.4 ${⊢}⟨{v},{u}⟩={C}\to \left({\chi }↔{\theta }\right)$
5 3optocl.5 ${⊢}\left(\left({x}\in {D}\wedge {y}\in {F}\right)\wedge \left({z}\in {D}\wedge {w}\in {F}\right)\wedge \left({v}\in {D}\wedge {u}\in {F}\right)\right)\to {\phi }$
6 4 imbi2d ${⊢}⟨{v},{u}⟩={C}\to \left(\left(\left({A}\in {R}\wedge {B}\in {R}\right)\to {\chi }\right)↔\left(\left({A}\in {R}\wedge {B}\in {R}\right)\to {\theta }\right)\right)$
7 2 imbi2d ${⊢}⟨{x},{y}⟩={A}\to \left(\left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\phi }\right)↔\left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\psi }\right)\right)$
8 3 imbi2d ${⊢}⟨{z},{w}⟩={B}\to \left(\left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\psi }\right)↔\left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\chi }\right)\right)$
9 5 3expia ${⊢}\left(\left({x}\in {D}\wedge {y}\in {F}\right)\wedge \left({z}\in {D}\wedge {w}\in {F}\right)\right)\to \left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\phi }\right)$
10 1 7 8 9 2optocl ${⊢}\left({A}\in {R}\wedge {B}\in {R}\right)\to \left(\left({v}\in {D}\wedge {u}\in {F}\right)\to {\chi }\right)$
11 10 com12 ${⊢}\left({v}\in {D}\wedge {u}\in {F}\right)\to \left(\left({A}\in {R}\wedge {B}\in {R}\right)\to {\chi }\right)$
12 1 6 11 optocl ${⊢}{C}\in {R}\to \left(\left({A}\in {R}\wedge {B}\in {R}\right)\to {\theta }\right)$
13 12 impcom ${⊢}\left(\left({A}\in {R}\wedge {B}\in {R}\right)\wedge {C}\in {R}\right)\to {\theta }$
14 13 3impa ${⊢}\left({A}\in {R}\wedge {B}\in {R}\wedge {C}\in {R}\right)\to {\theta }$