Theorem nfrab1 3318

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

Syntax hints:   ∧ wa 396   ∈ wcel 2107  {cab 2716  Ⅎwnfc 2888  {crab 3069

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rab 3074

This theorem is referenced by:  reusv2lem4  5325  reusv2  5327  rabxfrd  5341  riotaxfrd  7276  onminsb  7653  tfis  7710  oawordeulem  8394  nnawordex  8477  rankidb  9567  tskwe  9717  cardmin2  9766  cardaleph  9854  cardmin  10329  nnwos  12664  neiptopnei  22292  dissnlocfin  22689  imasnopn  22850  imasncld  22851  imasncls  22852  blval2  23727  iundisj  24721  mbfinf  24838  lfgrnloop  27504  difrab2  30854  rabexgfGS  30855  eqrrabd  30858  rabss3d  30870  iundisjf  30937  fimarab  30989  aciunf1  31009  fpwrelmap  31077  fpwrelmapffs  31078  iundisjfi  31126  locfinreflem  31799  zarcls  31833  ordtconnlem1  31883  esumrnmpt2  32045  esumpinfval  32050  hasheuni  32062  ldsysgenld  32137  measvuni  32191  eulerpartlemn  32357  ballotlem7  32511  ballotth  32513  reprdifc  32616  bnj1230  32791  bnj1476  32836  bnj1204  33001  bnj1311  33013  satfv1  33334  sltval2  33868  bj-rabtrALT  35128  topdifinfindis  35526  icorempo  35531  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlssretop  35543  phpreu  35770  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  cover2  35881  rababg  41188  rfcnpre1  42569  rfcnpre2  42581  ssrab2f  42673  infnsuprnmpt  42803  allbutfiinf  42967  supminfxr2  43016  fsumiunss  43123  limcperiod  43176  fnlimcnv  43215  fnlimfvre2  43225  fnlimf  43226  limsupequzmpt2  43266  liminfequzmpt2  43339  dvcosre  43460  stoweidlem14  43562  stoweidlem26  43574  stoweidlem31  43579  stoweidlem34  43582  stoweidlem35  43583  stoweidlem46  43594  stoweidlem50  43598  stoweidlem51  43599  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  stoweidlem57  43605  stoweidlem59  43607  fourierdlem20  43675  fourierdlem31  43686  fourierdlem79  43733  sge0iunmptlemre  43960  ovnlerp  44107  opnvonmbllem1  44177  preimagelt  44244  preimalegt  44245  pimconstlt1  44247  pimltpnff  44248  pimrecltpos  44253  pimiooltgt  44255  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  pimgtmnff  44267  pimrecltneg  44269  sssmf  44283  incsmflem  44286  issmfle  44290  issmfgt  44301  smfaddlem1  44308  decsmflem  44311  issmfge  44315  smflimlem2  44317  smflim  44322  smfresal  44333  smfmullem2  44337  smfmullem4  44339  smfpimbor1lem2  44344  smflim2  44350  smfpimcclem  44351  smfsup  44358  smfinf  44362  smflimsuplem2  44365  smflimsuplem5  44368  smflimsuplem7  44370  smflimsup  44372  smfliminf  44375  prmdvdsfmtnof1lem1  45047