# Metamath Proof Explorer

## Theorem optocl

Description: Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995)

Ref Expression
Hypotheses optocl.1 ${⊢}{D}={B}×{C}$
optocl.2 ${⊢}⟨{x},{y}⟩={A}\to \left({\phi }↔{\psi }\right)$
optocl.3 ${⊢}\left({x}\in {B}\wedge {y}\in {C}\right)\to {\phi }$
Assertion optocl ${⊢}{A}\in {D}\to {\psi }$

### Proof

Step Hyp Ref Expression
1 optocl.1 ${⊢}{D}={B}×{C}$
2 optocl.2 ${⊢}⟨{x},{y}⟩={A}\to \left({\phi }↔{\psi }\right)$
3 optocl.3 ${⊢}\left({x}\in {B}\wedge {y}\in {C}\right)\to {\phi }$
4 elxp3 ${⊢}{A}\in \left({B}×{C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩={A}\wedge ⟨{x},{y}⟩\in \left({B}×{C}\right)\right)$
5 opelxp ${⊢}⟨{x},{y}⟩\in \left({B}×{C}\right)↔\left({x}\in {B}\wedge {y}\in {C}\right)$
6 5 3 sylbi ${⊢}⟨{x},{y}⟩\in \left({B}×{C}\right)\to {\phi }$
7 6 2 syl5ib ${⊢}⟨{x},{y}⟩={A}\to \left(⟨{x},{y}⟩\in \left({B}×{C}\right)\to {\psi }\right)$
8 7 imp ${⊢}\left(⟨{x},{y}⟩={A}\wedge ⟨{x},{y}⟩\in \left({B}×{C}\right)\right)\to {\psi }$
9 8 exlimivv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩={A}\wedge ⟨{x},{y}⟩\in \left({B}×{C}\right)\right)\to {\psi }$
10 4 9 sylbi ${⊢}{A}\in \left({B}×{C}\right)\to {\psi }$
11 10 1 eleq2s ${⊢}{A}\in {D}\to {\psi }$