Theorem ecoptocl

Description: Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995)

	Ref	Expression
Hypotheses	ecoptocl.1	$$⊢S=\left(B\times C\right)/R$$
	ecoptocl.2	$$⊢\left[⟨x,y⟩\right]R=A\to \left(\phi \leftrightarrow \psi \right)$$
	ecoptocl.3	$$⊢\left(x\in B\wedge y\in C\right)\to \phi$$
Assertion	ecoptocl	$$⊢A\in S\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		ecoptocl.1	$$⊢S=\left(B\times C\right)/R$$
2		ecoptocl.2	$$⊢\left[⟨x,y⟩\right]R=A\to \left(\phi \leftrightarrow \psi \right)$$
3		ecoptocl.3	$$⊢\left(x\in B\wedge y\in C\right)\to \phi$$
4		elqsi	$$⊢A\in \left(\left(B\times C\right)/R\right)\to \exists z\in \left(B\times C\right)A=\left[z\right]R$$
5		eqid	$$⊢B\times C=B\times C$$
6		eceq1	$$⊢⟨x,y⟩=z\to \left[⟨x,y⟩\right]R=\left[z\right]R$$
7	6	eqeq2d	$$⊢⟨x,y⟩=z\to \left(A=\left[⟨x,y⟩\right]R\leftrightarrow A=\left[z\right]R\right)$$
8	7	imbi1d	$$⊢⟨x,y⟩=z\to \left(\left(A=\left[⟨x,y⟩\right]R\to \psi \right)\leftrightarrow \left(A=\left[z\right]R\to \psi \right)\right)$$
9	2	eqcoms	$$⊢A=\left[⟨x,y⟩\right]R\to \left(\phi \leftrightarrow \psi \right)$$
10	3 9	syl5ibcom	$$⊢\left(x\in B\wedge y\in C\right)\to \left(A=\left[⟨x,y⟩\right]R\to \psi \right)$$
11	5 8 10	optocl	$$⊢z\in \left(B\times C\right)\to \left(A=\left[z\right]R\to \psi \right)$$
12	11	rexlimiv	$$⊢\exists z\in \left(B\times C\right)A=\left[z\right]R\to \psi$$
13	4 12	syl	$$⊢A\in \left(\left(B\times C\right)/R\right)\to \psi$$
14	13 1	eleq2s	$$⊢A\in S\to \psi$$