MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab1 Structured version   Visualization version   GIF version

Theorem nfrab1 3120
Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
nfrab1 𝑥{𝑥𝐴𝜑}

Proof of Theorem nfrab1
StepHypRef Expression
1 df-rab 2920 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 nfab1 2765 . 2 𝑥{𝑥 ∣ (𝑥𝐴𝜑)}
31, 2nfcxfr 2761 1 𝑥{𝑥𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 1989  {cab 2607  wnfc 2750  {crab 2915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920
This theorem is referenced by:  reusv2lem4  4870  reusv2  4872  rabxfrd  4887  riotaxfrd  6639  onminsb  6996  tfis  7051  oawordeulem  7631  nnawordex  7714  rankidb  8660  tskwe  8773  cardmin2  8821  cardaleph  8909  cardmin  9383  nnwos  11752  neiptopnei  20930  dissnlocfin  21326  imasnopn  21487  imasncld  21488  imasncls  21489  blval2  22361  iundisj  23310  mbfinf  23426  lfgrnloop  26014  numclwlk1lem2  27214  difrab2  29323  rabexgfGS  29324  rabss3d  29335  iundisjf  29386  fimarab  29429  aciunf1  29447  fpwrelmap  29493  fpwrelmapffs  29494  iundisjfi  29540  locfinreflem  29892  ordtconnlem1  29955  esumrnmpt2  30115  esumpinfval  30120  hasheuni  30132  ldsysgenld  30208  measvuni  30262  eulerpartlemn  30428  ballotlem7  30582  ballotth  30584  reprdifc  30690  bnj1230  30858  bnj1476  30902  bnj1204  31065  bnj1311  31077  sltval2  31793  bj-rabtrALT  32911  topdifinfindis  33174  icorempt2  33179  isbasisrelowllem1  33183  isbasisrelowllem2  33184  relowlssretop  33191  phpreu  33373  poimirlem26  33415  poimirlem27  33416  mbfposadd  33437  cover2  33488  rababg  37705  rfcnpre1  39004  rfcnpre2  39016  ssrab2f  39126  infnsuprnmpt  39287  allbutfiinf  39466  supminfxr2  39518  fsumiunss  39613  limcperiod  39666  fnlimcnv  39705  fnlimfvre2  39715  fnlimf  39716  limsupequzmpt2  39756  liminfequzmpt2  39823  dvcosre  39895  stoweidlem14  40000  stoweidlem26  40012  stoweidlem31  40017  stoweidlem34  40020  stoweidlem35  40021  stoweidlem46  40032  stoweidlem50  40036  stoweidlem51  40037  stoweidlem52  40038  stoweidlem53  40039  stoweidlem54  40040  stoweidlem57  40043  stoweidlem59  40045  fourierdlem20  40113  fourierdlem31  40124  fourierdlem79  40171  sge0iunmptlemre  40401  ovnlerp  40545  opnvonmbllem1  40615  preimagelt  40681  preimalegt  40682  pimconstlt1  40684  pimltpnf  40685  pimrecltpos  40688  pimiooltgt  40690  pimdecfgtioc  40694  pimincfltioc  40695  pimdecfgtioo  40696  pimincfltioo  40697  preimageiingt  40699  preimaleiinlt  40700  pimrecltneg  40702  sssmf  40716  incsmflem  40719  issmfle  40723  issmfgt  40734  smfaddlem1  40740  decsmflem  40743  issmfge  40747  smflimlem2  40749  smflim  40754  smfresal  40764  smfmullem2  40768  smfmullem4  40770  smfpimbor1lem2  40775  smflim2  40781  smfpimcclem  40782  smfsup  40789  smfinf  40793  smflimsuplem2  40796  smflimsuplem3  40797  smflimsuplem5  40799  smflimsuplem7  40801  smflimsup  40803  smfliminf  40806  prmdvdsfmtnof1lem1  41267
  Copyright terms: Public domain W3C validator