Theorem elrabf

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003)

	Ref	Expression
Hypotheses	elrabf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	elrabf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	elrabf.3	$$⊢Ⅎx\psi$$
	elrabf.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	elrabf	$$⊢A\in \left\{x\in B|\phi \right\}\leftrightarrow \left(A\in B\wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elrabf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		elrabf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		elrabf.3	$$⊢Ⅎx\psi$$
4		elrabf.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
5		elex	$$⊢A\in \left\{x\in B|\phi \right\}\to A\in \mathrm{V}$$
6		elex	$$⊢A\in B\to A\in \mathrm{V}$$
7	6	adantr	$$⊢\left(A\in B\wedge \psi \right)\to A\in \mathrm{V}$$
8		df-rab	$$⊢\left\{x\in B|\phi \right\}=\left\{x|\left(x\in B\wedge \phi \right)\right\}$$
9	8	eleq2i	$$⊢A\in \left\{x\in B|\phi \right\}\leftrightarrow A\in \left\{x|\left(x\in B\wedge \phi \right)\right\}$$
10	1 2	nfel	$$⊢ℲxA\in B$$
11	10 3	nfan	$$⊢Ⅎx\left(A\in B\wedge \psi \right)$$
12		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
13	12 4	anbi12d	$$⊢x=A\to \left(\left(x\in B\wedge \phi \right)\leftrightarrow \left(A\in B\wedge \psi \right)\right)$$
14	1 11 13	elabgf	$$⊢A\in \mathrm{V}\to \left(A\in \left\{x|\left(x\in B\wedge \phi \right)\right\}\leftrightarrow \left(A\in B\wedge \psi \right)\right)$$
15	9 14	bitrid	$$⊢A\in \mathrm{V}\to \left(A\in \left\{x\in B|\phi \right\}\leftrightarrow \left(A\in B\wedge \psi \right)\right)$$
16	5 7 15	pm5.21nii	$$⊢A\in \left\{x\in B|\phi \right\}\leftrightarrow \left(A\in B\wedge \psi \right)$$