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

Theorem nfrab1 3365
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 3139 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 nfab1 2981 . 2 𝑥{𝑥 ∣ (𝑥𝐴𝜑)}
31, 2nfcxfr 2977 1 𝑥{𝑥𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 399  wcel 2114  {cab 2800  wnfc 2960  {crab 3134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139
This theorem is referenced by:  reusv2lem4  5279  reusv2  5281  rabxfrd  5295  riotaxfrd  7132  onminsb  7499  tfis  7554  oawordeulem  8167  nnawordex  8250  rankidb  9217  tskwe  9367  cardmin2  9416  cardaleph  9504  cardmin  9975  nnwos  12303  neiptopnei  21735  dissnlocfin  22132  imasnopn  22293  imasncld  22294  imasncls  22295  blval2  23167  iundisj  24150  mbfinf  24267  lfgrnloop  26916  difrab2  30266  rabexgfGS  30267  eqrrabd  30270  rabss3d  30283  iundisjf  30347  fimarab  30398  aciunf1  30416  fpwrelmap  30479  fpwrelmapffs  30480  iundisjfi  30529  locfinreflem  31162  zarcls  31196  ordtconnlem1  31241  esumrnmpt2  31401  esumpinfval  31406  hasheuni  31418  ldsysgenld  31493  measvuni  31547  eulerpartlemn  31713  ballotlem7  31867  ballotth  31869  reprdifc  31972  bnj1230  32148  bnj1476  32193  bnj1204  32358  bnj1311  32370  satfv1  32684  sltval2  33237  bj-rabtrALT  34334  topdifinfindis  34724  icorempo  34729  isbasisrelowllem1  34733  isbasisrelowllem2  34734  relowlssretop  34741  phpreu  34999  poimirlem26  35041  poimirlem27  35042  mbfposadd  35062  cover2  35110  rababg  40203  rfcnpre1  41582  rfcnpre2  41594  ssrab2f  41688  infnsuprnmpt  41826  allbutfiinf  41996  supminfxr2  42047  fsumiunss  42156  limcperiod  42209  fnlimcnv  42248  fnlimfvre2  42258  fnlimf  42259  limsupequzmpt2  42299  liminfequzmpt2  42372  dvcosre  42493  stoweidlem14  42595  stoweidlem26  42607  stoweidlem31  42612  stoweidlem34  42615  stoweidlem35  42616  stoweidlem46  42627  stoweidlem50  42631  stoweidlem51  42632  stoweidlem52  42633  stoweidlem53  42634  stoweidlem54  42635  stoweidlem57  42638  stoweidlem59  42640  fourierdlem20  42708  fourierdlem31  42719  fourierdlem79  42766  sge0iunmptlemre  42993  ovnlerp  43140  opnvonmbllem1  43210  preimagelt  43276  preimalegt  43277  pimconstlt1  43279  pimltpnf  43280  pimrecltpos  43283  pimiooltgt  43285  pimdecfgtioc  43289  pimincfltioc  43290  pimdecfgtioo  43291  pimincfltioo  43292  preimageiingt  43294  preimaleiinlt  43295  pimrecltneg  43297  sssmf  43311  incsmflem  43314  issmfle  43318  issmfgt  43329  smfaddlem1  43335  decsmflem  43338  issmfge  43342  smflimlem2  43344  smflim  43349  smfresal  43359  smfmullem2  43363  smfmullem4  43365  smfpimbor1lem2  43370  smflim2  43376  smfpimcclem  43377  smfsup  43384  smfinf  43388  smflimsuplem2  43391  smflimsuplem5  43394  smflimsuplem7  43396  smflimsup  43398  smfliminf  43401  prmdvdsfmtnof1lem1  44040
  Copyright terms: Public domain W3C validator