Theorem nfrab1 3449

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

Syntax hints:   ∧ wa 394   ∈ wcel 2104  {cab 2707  Ⅎwnfc 2881  {crab 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431

This theorem is referenced by:  rabss3d  4078  reusv2lem4  5398  reusv2  5400  rabxfrd  5414  riotaxfrd  7402  onminsb  7784  tfis  7846  oawordeulem  8556  nnawordex  8639  rankidb  9797  tskwe  9947  cardmin2  9996  cardaleph  10086  cardmin  10561  nnwos  12903  neiptopnei  22856  dissnlocfin  23253  imasnopn  23414  imasncld  23415  imasncls  23416  blval2  24291  iundisj  25297  mbfinf  25414  sltval2  27395  lfgrnloop  28652  difrab2  32005  rabexgfGS  32006  eqrrabd  32008  iundisjf  32087  fimarab  32135  aciunf1  32155  fpwrelmap  32225  fpwrelmapffs  32226  iundisjfi  32274  algextdeglem6  33067  locfinreflem  33118  zarcls  33152  ordtconnlem1  33202  esumrnmpt2  33364  esumpinfval  33369  hasheuni  33381  ldsysgenld  33456  measvuni  33510  eulerpartlemn  33678  ballotlem7  33832  ballotth  33834  reprdifc  33937  bnj1230  34111  bnj1476  34156  bnj1204  34321  bnj1311  34333  satfv1  34652  bj-rabtrALT  36114  topdifinfindis  36530  icorempo  36535  isbasisrelowllem1  36539  isbasisrelowllem2  36540  relowlssretop  36547  phpreu  36775  poimirlem26  36817  poimirlem27  36818  mbfposadd  36838  cover2  36886  naddwordnexlem4  42454  rababg  42627  rfcnpre1  44005  rfcnpre2  44017  ssrab2f  44107  infnsuprnmpt  44252  allbutfiinf  44428  supminfxr2  44477  pimxrneun  44497  fsumiunss  44589  limcperiod  44642  fnlimcnv  44681  fnlimfvre2  44691  fnlimf  44692  limsupequzmpt2  44732  liminfequzmpt2  44805  dvcosre  44926  stoweidlem14  45028  stoweidlem26  45040  stoweidlem31  45045  stoweidlem34  45048  stoweidlem35  45049  stoweidlem46  45060  stoweidlem50  45064  stoweidlem51  45065  stoweidlem52  45066  stoweidlem53  45067  stoweidlem54  45068  stoweidlem57  45071  stoweidlem59  45073  fourierdlem20  45141  fourierdlem31  45152  fourierdlem79  45199  sge0iunmptlemre  45429  ovnlerp  45576  opnvonmbllem1  45646  preimagelt  45713  preimalegt  45714  pimconstlt1  45716  pimltpnff  45717  pimrecltpos  45722  pimiooltgt  45724  pimdecfgtioc  45729  pimincfltioc  45730  pimdecfgtioo  45731  pimincfltioo  45732  preimageiingt  45734  preimaleiinlt  45735  pimgtmnff  45736  pimrecltneg  45738  sssmf  45752  incsmflem  45755  issmfle  45759  issmfgt  45770  smfaddlem1  45777  decsmflem  45780  issmfge  45784  smflimlem2  45786  smflim  45791  smfresal  45802  smfmullem2  45806  smfmullem4  45808  smfpimbor1lem2  45813  smflim2  45820  smfpimcclem  45821  smfsup  45828  smfinf  45832  smflimsuplem2  45835  smflimsuplem5  45838  smflimsuplem7  45840  smflimsup  45842  smfliminf  45845  smfdivdmmbl2  45855  fsupdm  45856  fsupdm2  45857  finfdm  45860  finfdm2  45861  prmdvdsfmtnof1lem1  46550