Theorem nfrab 2984

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 2758	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1688	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2597	. . . . . . 7 |- F/ x z e. A
5		eleq1 2528	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2184	. . . . . 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 2019	. . . . 5 |- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl 472	. . . 4 |- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	2, 10	nfabd2 2622	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1464	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2601	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 375   A.wal 1453   T. wtru 1456   F/wnf 1678   e. wcel 1898   {cab 2448   F/_wnfc 2590   {crab 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758

This theorem is referenced by:  nfdif  3566  nfin  3651  nfse  4831  elfvmptrab1  5998  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rab1  6557  elovmpt3rab1  6559  mpt2xopoveq  6997  nfoi  8060  scottex  8387  elmptrab  20897  iundisjf  28253  nnindf  28434  bnj1398  29893  bnj1445  29903  bnj1449  29907  nfwlim  30555  finminlem  31024  poimirlem26  32012  poimirlem27  32013  indexa  32106  binomcxplemdvbinom  36747  binomcxplemdvsum  36749  binomcxplemnotnn0  36750  dvnprodlem1  37907  stoweidlem16  37977  stoweidlem31  37993  stoweidlem34  37996  stoweidlem35  37997  stoweidlem48  38010  stoweidlem51  38013  stoweidlem53  38015  stoweidlem54  38016  stoweidlem57  38019  stoweidlem59  38021  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem48  38119  fourierdlem51  38122  etransclem32  38232  ovncvrrp  38493