Theorem nfrab 3008

Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

Ref	Expression
nfrab.1	|- F/ x ph
nfrab.2	|- F/_ x A

Assertion

Ref	Expression
nfrab	|- F/_ x { y e. A | ph }

Proof of Theorem nfrab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 2808	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1600	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2609	. . . . . . 7 |- F/ x z e. A
5		eleq1 2526	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2041	. . . . . 6 |- ( -. A. x x = y -> F/ x y e. A )
7		nfrab.1	. . . . . . 7 |- F/ x ph
8	7	a1i 11	. . . . . 6 |- ( -. A. x x = y -> F/ x ph )
9	6, 8	nfand 1863	. . . . 5 |- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl 466	. . . 4 |- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	2, 10	nfabd2 2637	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1379	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2614	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 369   A.wal 1368   T. wtru 1371   F/wnf 1590   e. wcel 1758   {cab 2439   F/_wnfc 2602   {crab 2803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808

This theorem is referenced by:  nfdif  3588  nfin  3668  reusv6OLD  4614  nfse  4806  mpt2xopoveq  6849  nfoi  7843  scottex  8207  elmptrab  19542  iundisjf  26109  nnindf  26261  nfwlim  27926  finminlem  28684  indexa  28798  stoweidlem16  29982  stoweidlem31  29997  stoweidlem34  30000  stoweidlem35  30001  stoweidlem48  30014  stoweidlem51  30017  stoweidlem53  30019  stoweidlem54  30020  stoweidlem57  30023  stoweidlem59  30025  elfvmptrab1  30325  elovmpt2rab  30329  elovmpt2rab1  30330  ovmpt3rab1  30332  elovmpt3rab1  30334  bnj1398  32380  bnj1445  32390  bnj1449  32394