Theorem nfrab1 3436

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

Step	Hyp	Ref	Expression
1		df-rab 3417	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		nfab1 2927	. 2 ⊢ Ⅎ𝑥{𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	1, 2	nfcxfr 2923	1 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 400   ∈ wcel 2143  {cab 2741  Ⅎwnfc 2910  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417

This theorem is referenced by:  rabss3d  4036  eqrrabd  4041  reusv2lem4  5374  reusv2  5376  rabxfrd  5390  fimarab  6957  riotaxfrd  7403  onminsb  7794  tfis  7852  oawordeulem  8540  nnawordex  8624  rankidb  9773  tskwe  9937  cardmin2  9986  cardaleph  10074  cardmin  10549  nnwos  12940  rspsn0  21353  neiptopnei  23270  dissnlocfin  23667  imasnopn  23828  imasncld  23829  imasncls  23830  blval2  24700  iundisj  25688  mbfinf  25805  ltsval2  27801  lfgrnloop  29456  difrab2  32825  rabexgfGS  32826  iundisjf  32915  aciunf1  32989  fpwrelmap  33059  fpwrelmapffs  33060  iundisjfi  33122  algextdeglem6  34093  constrfin  34117  locfinreflem  34211  zarcls  34245  ordtconnlem1  34295  esumrnmpt2  34439  esumpinfval  34444  hasheuni  34456  ldsysgenld  34531  measvuni  34585  eulerpartlemn  34752  ballotlem7  34907  ballotth  34909  reprdifc  34995  bnj1230  35171  bnj1476  35216  bnj1204  35381  bnj1311  35393  onvf1odlem2  35569  vonf1oonfo  35580  satfv1  35836  bj-rabtrALT  37548  topdifinfindis  37973  icorempo  37978  isbasisrelowllem1  37982  isbasisrelowllem2  37983  relowlssretop  37990  phpreu  38236  poimirlem26  38278  poimirlem27  38279  mbfposadd  38299  cover2  38347  naddwordnexlem4  44111  rababg  44283  permaxsep  45699  rfcnpre1  45722  rfcnpre2  45734  ssrab2f  45818  infnsuprnmpt  45948  allbutfiinf  46117  supminfxr2  46166  pimxrneun  46185  limcperiod  46327  fnlimcnv  46364  fnlimfvre2  46374  fnlimf  46375  limsupequzmpt2  46415  liminfequzmpt2  46488  dvcosre  46609  stoweidlem14  46711  stoweidlem26  46723  stoweidlem31  46728  stoweidlem34  46731  stoweidlem35  46732  stoweidlem46  46743  stoweidlem50  46747  stoweidlem51  46748  stoweidlem52  46749  stoweidlem53  46750  stoweidlem54  46751  stoweidlem57  46754  stoweidlem59  46756  fourierdlem20  46824  fourierdlem31  46835  fourierdlem79  46882  sge0iunmptlemre  47112  ovnlerp  47259  opnvonmbllem1  47329  preimagelt  47396  preimalegt  47397  pimconstlt1  47399  pimltpnff  47400  pimrecltpos  47405  pimiooltgt  47407  pimdecfgtioc  47412  pimincfltioc  47413  pimdecfgtioo  47414  pimincfltioo  47415  preimageiingt  47417  preimaleiinlt  47418  pimgtmnff  47419  pimrecltneg  47421  sssmf  47435  incsmflem  47438  issmfle  47442  issmfgt  47453  smfaddlem1  47460  decsmflem  47463  issmfge  47467  smflimlem2  47469  smflim  47474  smfresal  47485  smfmullem2  47489  smfmullem4  47491  smfpimbor1lem2  47496  smflim2  47503  smfpimcclem  47504  smfsup  47511  smfinf  47515  smflimsuplem2  47518  smflimsuplem5  47521  smflimsuplem7  47523  smflimsup  47525  smfliminf  47528  smfdivdmmbl2  47538  fsupdm  47539  fsupdm2  47540  finfdm  47543  finfdm2  47544  prmdvdsfmtnof1lem1  48319