ectocld

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

Step	Hyp	Ref	Expression
1		ectocl.1	$⊢ S = B / R$
2		ectocl.2	$⊢ [x] R = A \to (φ \leftrightarrow ψ)$
3		ectocld.3	$⊢ (χ \land x \in B) \to φ$
4	2	eqcoms	$⊢ A = [x] R \to (φ \leftrightarrow ψ)$
5	3 4	syl5ibcom	$⊢ (χ \land x \in B) \to (A = [x] R \to ψ)$
6	5	rexlimdva	$⊢ χ \to (\exists x \in B A = [x] R \to ψ)$
7		elqsi	$⊢ A \in (B / R) \to \exists x \in B A = [x] R$
8	7 1	eleq2s	$⊢ A \in S \to \exists x \in B A = [x] R$
9	6 8	impel	$⊢ (χ \land A \in S) \to ψ$

Metamath Proof Explorer