Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab Unicode version

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.
StepHypRef Expression
1 df-rab 2816 . 2
2 nftru 1626 . . . 4
3 nfrab.2 . . . . . . . 8
43nfcri 2612 . . . . . . 7
5 eleq1 2529 . . . . . . 7
64, 5dvelimnf 2081 . . . . . 6
7 nfrab.1 . . . . . . 7
87a1i 11 . . . . . 6
96, 8nfand 1925 . . . . 5
109adantl 466 . . . 4
112, 10nfabd2 2640 . . 3
1211trud 1404 . 2
131, 12nfcxfr 2617 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator