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

Proof

Step	Hyp	Ref	Expression
1		ectocl.1	|- S = ( B /. R )
2		ectocl.2	|- ( [ x ] R = A -> ( ph <-> ps ) )
3		ectocl.3	|- ( x e. B -> ph )
4		tru	|- T.
5	3	adantl	|- ( ( T. /\ x e. B ) -> ph )
6	1 2 5	ectocld	|- ( ( T. /\ A e. S ) -> ps )
7	4 6	mpan	|- ( A e. S -> ps )