Theorem rabexgf

Description: A version of rabexg using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypothesis	rabexgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	rabexgf	$$⊢A\in V\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rabexgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
3		simpl	$$⊢\left(x\in A\wedge \phi \right)\to x\in A$$
4	3	ss2abi	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq \left\{x|x\in A\right\}$$
5	1	abid2f	$$⊢\left\{x|x\in A\right\}=A$$
6	4 5	sseqtri	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$
7	2 6	eqsstri	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$
8		ssexg	$$⊢\left(\left\{x\in A|\phi \right\}\subseteq A\wedge A\in V\right)\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$
9	7 8	mpan	$$⊢A\in V\to \left\{x\in A|\phi \right\}\in \mathrm{V}$$