Theorem elrabsf

Description: Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf has implicit substitution). The hypothesis specifies that x must not be a free variable in B . (Contributed by NM, 30-Sep-2003) (Proof shortened by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypothesis	elrabsf.1	|- F/_ x B
Assertion	elrabsf	|- ( A e. { x e. B | ph } <-> ( A e. B /\ [. A / x ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		elrabsf.1	|- F/_ x B
2		dfsbcq	|- ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
3		nfcv	|- F/_ y B
4		nfv	|- F/ y ph
5		nfsbc1v	|- F/ x [. y / x ]. ph
6		sbceq1a	|- ( x = y -> ( ph <-> [. y / x ]. ph ) )
7	1 3 4 5 6	cbvrabw	|- { x e. B | ph } = { y e. B | [. y / x ]. ph }
8	2 7	elrab2	|- ( A e. { x e. B | ph } <-> ( A e. B /\ [. A / x ]. ph ) )