Theorem nfrab 3123

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 2921	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1730	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2758	. . . . . . 7 |- F/ x z e. A
5		eleq1 2689	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2339	. . . . . 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 1826	. . . . 5 |- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl 482	. . . 4 |- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	2, 10	nfabd2 2784	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1493	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2762	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 384   A.wal 1481   T. wtru 1484   F/wnf 1708   e. wcel 1990   {cab 2608   F/_wnfc 2751   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921

This theorem is referenced by:  nfdif  3731  nfin  3820  nfse  5089  elfvmptrab1  6305  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rab1  6891  elovmpt3rab1  6893  mpt2xopoveq  7345  nfoi  8419  scottex  8748  elmptrab  21630  iundisjf  29402  nnindf  29565  bnj1398  31102  bnj1445  31112  bnj1449  31116  nfwlim  31768  finminlem  32312  poimirlem26  33435  poimirlem27  33436  indexa  33528  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  infnsuprnmpt  39465  allbutfiinf  39647  supminfrnmpt  39672  supminfxrrnmpt  39701  fnlimfvre  39906  fnlimabslt  39911  dvnprodlem1  40161  stoweidlem16  40233  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem48  40265  stoweidlem51  40268  stoweidlem53  40270  stoweidlem54  40271  stoweidlem57  40274  stoweidlem59  40276  fourierdlem31  40355  fourierdlem48  40371  fourierdlem51  40374  etransclem32  40483  ovncvrrp  40778  smflim  40985  smflimmpt  41016  smfsupmpt  41021  smfsupxr  41022  smfinfmpt  41025  smflimsuplem7  41032