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	|- ( [ x ] R = A -> ( ph <-> ps ) )
	ectocld.3	|- ( ( ch /\ x e. B ) -> ph )
Assertion	ectocld	|- ( ( ch /\ A e. S ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		ectocl.1	|- S = ( B /. R )
2		ectocl.2	|- ( [ x ] R = A -> ( ph <-> ps ) )
3		ectocld.3	|- ( ( ch /\ x e. B ) -> ph )
4	2	eqcoms	|- ( A = [ x ] R -> ( ph <-> ps ) )
5	3 4	syl5ibcom	|- ( ( ch /\ x e. B ) -> ( A = [ x ] R -> ps ) )
6	5	rexlimdva	|- ( ch -> ( E. x e. B A = [ x ] R -> ps ) )
7		elqsi	|- ( A e. ( B /. R ) -> E. x e. B A = [ x ] R )
8	7 1	eleq2s	|- ( A e. S -> E. x e. B A = [ x ] R )
9	6 8	impel	|- ( ( ch /\ A e. S ) -> ps )