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

Theorem nfrab 2881
 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 2706 . 2
2 nftru 1563 . . . 4
3 nfrab.2 . . . . . . . 8
43nfcri 2565 . . . . . . 7
5 eleq1 2495 . . . . . . 7
64, 5dvelimnf 2071 . . . . . 6
7 nfrab.1 . . . . . . 7
87a1i 11 . . . . . 6
96, 8nfand 1843 . . . . 5
109adantl 453 . . . 4
112, 10nfabd2 2589 . . 3
1211trud 1332 . 2
131, 12nfcxfr 2568 1
 Colors of variables: wff set class Syntax hints:   wn 3   wa 359   wtru 1325  wal 1549  wnf 1553   wcel 1725  cab 2421  wnfc 2558  crab 2701 This theorem is referenced by:  nfdif  3460  nfin  3539  nfse  4549  reusv6OLD  4726  mpt2xopoveq  6462  nfoi  7475  scottex  7801  elmptrab  17851  iundisjf  24021  nfwlim  25565  finminlem  26302  indexa  26416  stoweidlem16  27722  stoweidlem31  27737  stoweidlem34  27740  stoweidlem35  27741  stoweidlem48  27754  stoweidlem51  27757  stoweidlem53  27759  stoweidlem54  27760  stoweidlem57  27763  stoweidlem59  27765  bnj1398  29330  bnj1445  29340  bnj1449  29344 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706
 Copyright terms: Public domain W3C validator