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	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	elrabsf	$$⊢A\in \left\{x\in B|\phi \right\}\leftrightarrow \left(A\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elrabsf.1	$$⊢\underset{\_}{Ⅎ}xB$$
2		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
4		nfv	$$⊢Ⅎy\phi$$
5		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
6		sbceq1a	$$⊢x=y\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
7	1 3 4 5 6	cbvrabw	$$⊢\left\{x\in B|\phi \right\}=\left\{y\in B|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right\}$$
8	2 7	elrab2	$$⊢A\in \left\{x\in B|\phi \right\}\leftrightarrow \left(A\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$