Theorem nfrab 3048

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 2826	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1609	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2622	. . . . . . 7 |- F/ x z e. A
5		eleq1 2539	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2054	. . . . . 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 1872	. . . . 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 2650	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1388	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2627	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 369   A.wal 1377   T. wtru 1380   F/wnf 1599   e. wcel 1767   {cab 2452   F/_wnfc 2615   {crab 2821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826

This theorem is referenced by:  nfdif  3630  nfin  3710  reusv6OLD  4664  nfse  4860  elfvmptrab1  5977  elovmpt2rab  6516  elovmpt2rab1  6517  ovmpt3rab1  6529  elovmpt3rab1  6531  mpt2xopoveq  6959  nfoi  7951  scottex  8315  elmptrab  20196  iundisjf  27271  nnindf  27434  nfwlim  29305  finminlem  30063  indexa  30151  stoweidlem16  31639  stoweidlem31  31654  stoweidlem34  31657  stoweidlem35  31658  stoweidlem48  31671  stoweidlem51  31674  stoweidlem53  31676  stoweidlem54  31677  stoweidlem57  31680  stoweidlem59  31682  fourierdlem31  31761  fourierdlem48  31778  fourierdlem51  31781  bnj1398  33570  bnj1445  33580  bnj1449  33584