Theorem nfrab 3007

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 2780	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1671	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2573	. . . . . . 7 |- F/ x z e. A
5		eleq1 2495	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2140	. . . . . 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 1985	. . . . 5 |- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl 467	. . . 4 |- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	2, 10	nfabd2 2601	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1446	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2578	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 370   A.wal 1435   T. wtru 1438   F/wnf 1661   e. wcel 1872   {cab 2407   F/_wnfc 2566   {crab 2775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780

This theorem is referenced by:  nfdif  3586  nfin  3669  nfse  4828  elfvmptrab1  5986  elovmpt2rab  6529  elovmpt2rab1  6530  ovmpt3rab1  6539  elovmpt3rab1  6541  mpt2xopoveq  6976  nfoi  8038  scottex  8364  elmptrab  20840  iundisjf  28201  nnindf  28389  bnj1398  29851  bnj1445  29861  bnj1449  29865  nfwlim  30512  finminlem  30979  poimirlem26  31930  poimirlem27  31931  indexa  32024  binomcxplemdvbinom  36672  binomcxplemdvsum  36674  binomcxplemnotnn0  36675  dvnprodlem1  37761  stoweidlem16  37816  stoweidlem31  37832  stoweidlem34  37835  stoweidlem35  37836  stoweidlem48  37849  stoweidlem51  37852  stoweidlem53  37854  stoweidlem54  37855  stoweidlem57  37858  stoweidlem59  37860  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem48  37958  fourierdlem51  37961  etransclem32  38071  ovncvrrp  38290