Theorem nfrab 3039

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
nfrab.2

Assertion

Ref	Expression
nfrab

Proof of Theorem nfrab

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 2816	. 2
2		nftru 1626	. . . 4
3		nfrab.2	. . . . . . . 8
4	3	nfcri 2612	. . . . . . 7
5		eleq1 2529	. . . . . . 7
6	4, 5	dvelimnf 2081	. . . . . 6
7		nfrab.1	. . . . . . 7
8	7	a1i 11	. . . . . 6
9	6, 8	nfand 1925	. . . . 5
10	9	adantl 466	. . . 4
11	2, 10	nfabd2 2640	. . 3
12	11	trud 1404	. 2
13	1, 12	nfcxfr 2617	1

Syntax hints:  -.wn 3  /\wa 369  A.wal 1393  wtru 1396  F/wnf 1616  e.wcel 1818  {cab 2442  F/_wnfc 2605  {crab 2811

This theorem is referenced by:  nfdif  3624  nfin  3704  reusv6OLD  4663  nfse  4859  elfvmptrab1  5976  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rab1  6534  elovmpt3rab1  6536  mpt2xopoveq  6966  nfoi  7960  scottex  8324  elmptrab  20328  iundisjf  27448  nnindf  27610  nfwlim  29378  finminlem  30136  indexa  30224  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  dvnprodlem1  31743  stoweidlem16  31798  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem48  31830  stoweidlem51  31833  stoweidlem53  31835  stoweidlem54  31836  stoweidlem57  31839  stoweidlem59  31841  fourierdlem31  31920  fourierdlem48  31937  fourierdlem51  31940  etransclem32  32049  bnj1398  34090  bnj1445  34100  bnj1449  34104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816