Theorem nfrab1 3452

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 3434	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		nfab1 2906	. 2 ⊢ Ⅎ𝑥{𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	1, 2	nfcxfr 2902	1 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 397   ∈ wcel 2107  {cab 2710  Ⅎwnfc 2884  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434

This theorem is referenced by:  rabss3d  4080  reusv2lem4  5400  reusv2  5402  rabxfrd  5416  riotaxfrd  7400  onminsb  7782  tfis  7844  oawordeulem  8554  nnawordex  8637  rankidb  9795  tskwe  9945  cardmin2  9994  cardaleph  10084  cardmin  10559  nnwos  12899  neiptopnei  22636  dissnlocfin  23033  imasnopn  23194  imasncld  23195  imasncls  23196  blval2  24071  iundisj  25065  mbfinf  25182  sltval2  27159  lfgrnloop  28385  difrab2  31738  rabexgfGS  31739  eqrrabd  31741  iundisjf  31820  fimarab  31868  aciunf1  31888  fpwrelmap  31958  fpwrelmapffs  31959  iundisjfi  32007  locfinreflem  32820  zarcls  32854  ordtconnlem1  32904  esumrnmpt2  33066  esumpinfval  33071  hasheuni  33083  ldsysgenld  33158  measvuni  33212  eulerpartlemn  33380  ballotlem7  33534  ballotth  33536  reprdifc  33639  bnj1230  33813  bnj1476  33858  bnj1204  34023  bnj1311  34035  satfv1  34354  bj-rabtrALT  35811  topdifinfindis  36227  icorempo  36232  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlssretop  36244  phpreu  36472  poimirlem26  36514  poimirlem27  36515  mbfposadd  36535  cover2  36583  naddwordnexlem4  42152  rababg  42325  rfcnpre1  43703  rfcnpre2  43715  ssrab2f  43806  infnsuprnmpt  43954  allbutfiinf  44130  supminfxr2  44179  pimxrneun  44199  fsumiunss  44291  limcperiod  44344  fnlimcnv  44383  fnlimfvre2  44393  fnlimf  44394  limsupequzmpt2  44434  liminfequzmpt2  44507  dvcosre  44628  stoweidlem14  44730  stoweidlem26  44742  stoweidlem31  44747  stoweidlem34  44750  stoweidlem35  44751  stoweidlem46  44762  stoweidlem50  44766  stoweidlem51  44767  stoweidlem52  44768  stoweidlem53  44769  stoweidlem54  44770  stoweidlem57  44773  stoweidlem59  44775  fourierdlem20  44843  fourierdlem31  44854  fourierdlem79  44901  sge0iunmptlemre  45131  ovnlerp  45278  opnvonmbllem1  45348  preimagelt  45415  preimalegt  45416  pimconstlt1  45418  pimltpnff  45419  pimrecltpos  45424  pimiooltgt  45426  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  preimageiingt  45436  preimaleiinlt  45437  pimgtmnff  45438  pimrecltneg  45440  sssmf  45454  incsmflem  45457  issmfle  45461  issmfgt  45472  smfaddlem1  45479  decsmflem  45482  issmfge  45486  smflimlem2  45488  smflim  45493  smfresal  45504  smfmullem2  45508  smfmullem4  45510  smfpimbor1lem2  45515  smflim2  45522  smfpimcclem  45523  smfsup  45530  smfinf  45534  smflimsuplem2  45537  smflimsuplem5  45540  smflimsuplem7  45542  smflimsup  45544  smfliminf  45547  smfdivdmmbl2  45557  fsupdm  45558  fsupdm2  45559  finfdm  45562  finfdm2  45563  prmdvdsfmtnof1lem1  46252