Theorem ectocld

Description: Implicit substitution of class for equivalence class. (Contributed 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)$$
	ectocld.3	$$⊢\left(\chi \wedge x\in B\right)\to \phi$$
Assertion	ectocld	$$⊢\left(\chi \wedge A\in S\right)\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		ectocld.3	$$⊢\left(\chi \wedge x\in B\right)\to \phi$$
4	2	eqcoms	$$⊢A=\left[x\right]R\to \left(\phi \leftrightarrow \psi \right)$$
5	3 4	syl5ibcom	$$⊢\left(\chi \wedge x\in B\right)\to \left(A=\left[x\right]R\to \psi \right)$$
6	5	rexlimdva	$$⊢\chi \to \left(\exists x\in BA=\left[x\right]R\to \psi \right)$$
7		elqsi	$$⊢A\in \left(B/R\right)\to \exists x\in BA=\left[x\right]R$$
8	7 1	eleq2s	$$⊢A\in S\to \exists x\in BA=\left[x\right]R$$
9	6 8	impel	$$⊢\left(\chi \wedge A\in S\right)\to \psi$$