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	|- F/_ x A
Assertion	rabexgf	|- ( A e. V -> { x e. A | ph } e. _V )

Proof

Step	Hyp	Ref	Expression
1		rabexgf.1	|- F/_ x A
2		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3		simpl	|- ( ( x e. A /\ ph ) -> x e. A )
4	3	ss2abi	|- { x | ( x e. A /\ ph ) } C_ { x | x e. A }
5	1	abid2f	|- { x | x e. A } = A
6	4 5	sseqtri	|- { x | ( x e. A /\ ph ) } C_ A
7	2 6	eqsstri	|- { x e. A | ph } C_ A
8		ssexg	|- ( ( { x e. A | ph } C_ A /\ A e. V ) -> { x e. A | ph } e. _V )
9	7 8	mpan	|- ( A e. V -> { x e. A | ph } e. _V )