Theorem optocl

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

	Ref	Expression
Hypotheses	optocl.1	$$⊢D=B\times C$$
	optocl.2	$$⊢⟨x,y⟩=A\to \left(\phi \leftrightarrow \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\times C$$
2		optocl.2	$$⊢⟨x,y⟩=A\to \left(\phi \leftrightarrow \psi \right)$$
3		optocl.3	$$⊢\left(x\in B\wedge y\in C\right)\to \phi$$
4		elxp3	$$⊢A\in \left(B\times C\right)\leftrightarrow \exists x\exists y\left(⟨x,y⟩=A\wedge ⟨x,y⟩\in \left(B\times C\right)\right)$$
5		opelxp	$$⊢⟨x,y⟩\in \left(B\times C\right)\leftrightarrow \left(x\in B\wedge y\in C\right)$$
6	5 3	sylbi	$$⊢⟨x,y⟩\in \left(B\times C\right)\to \phi$$
7	6 2	imbitrid	$$⊢⟨x,y⟩=A\to \left(⟨x,y⟩\in \left(B\times C\right)\to \psi \right)$$
8	7	imp	$$⊢\left(⟨x,y⟩=A\wedge ⟨x,y⟩\in \left(B\times C\right)\right)\to \psi$$
9	8	exlimivv	$$⊢\exists x\exists y\left(⟨x,y⟩=A\wedge ⟨x,y⟩\in \left(B\times C\right)\right)\to \psi$$
10	4 9	sylbi	$$⊢A\in \left(B\times C\right)\to \psi$$
11	10 1	eleq2s	$$⊢A\in D\to \psi$$