Theorem ectocl

Description: Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypotheses	ectocl.1	$$⊢S=B/R$$
	ectocl.2	$$⊢\left[x\right]R=A\to \left(\phi \leftrightarrow \psi \right)$$
	ectocl.3	$$⊢x\in B\to \phi$$
Assertion	ectocl	$$⊢A\in S\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		ectocl.1	$$⊢S=B/R$$
2		ectocl.2	$$⊢\left[x\right]R=A\to \left(\phi \leftrightarrow \psi \right)$$
3		ectocl.3	$$⊢x\in B\to \phi$$
4		tru	$$⊢\top$$
5	3	adantl	$$⊢\left(\top \wedge x\in B\right)\to \phi$$
6	1 2 5	ectocld	$$⊢\left(\top \wedge A\in S\right)\to \psi$$
7	4 6	mpan	$$⊢A\in S\to \psi$$