Theorem nfrab1 3453

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

Syntax hints:   ∧ wa 395   ∈ wcel 2105  {cab 2711  Ⅎwnfc 2887  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433

This theorem is referenced by:  rabss3d  4090  eqrrabd  4095  reusv2lem4  5406  reusv2  5408  rabxfrd  5422  fimarab  6982  riotaxfrd  7421  onminsb  7813  tfis  7875  oawordeulem  8590  nnawordex  8673  rankidb  9837  tskwe  9987  cardmin2  10036  cardaleph  10126  cardmin  10601  nnwos  12954  neiptopnei  23155  dissnlocfin  23552  imasnopn  23713  imasncld  23714  imasncls  23715  blval2  24590  iundisj  25596  mbfinf  25713  sltval2  27715  lfgrnloop  29156  difrab2  32525  rabexgfGS  32526  iundisjf  32608  aciunf1  32679  fpwrelmap  32750  fpwrelmapffs  32751  iundisjfi  32803  algextdeglem6  33727  constrfin  33750  locfinreflem  33800  zarcls  33834  ordtconnlem1  33884  esumrnmpt2  34048  esumpinfval  34053  hasheuni  34065  ldsysgenld  34140  measvuni  34194  eulerpartlemn  34362  ballotlem7  34516  ballotth  34518  reprdifc  34620  bnj1230  34794  bnj1476  34839  bnj1204  35004  bnj1311  35016  satfv1  35347  bj-rabtrALT  36913  topdifinfindis  37328  icorempo  37333  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  phpreu  37590  poimirlem26  37632  poimirlem27  37633  mbfposadd  37653  cover2  37701  naddwordnexlem4  43390  rababg  43563  rfcnpre1  44956  rfcnpre2  44968  ssrab2f  45056  infnsuprnmpt  45194  allbutfiinf  45369  supminfxr2  45418  pimxrneun  45438  limcperiod  45583  fnlimcnv  45622  fnlimfvre2  45632  fnlimf  45633  limsupequzmpt2  45673  liminfequzmpt2  45746  dvcosre  45867  stoweidlem14  45969  stoweidlem26  45981  stoweidlem31  45986  stoweidlem34  45989  stoweidlem35  45990  stoweidlem46  46001  stoweidlem50  46005  stoweidlem51  46006  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  stoweidlem57  46012  stoweidlem59  46014  fourierdlem20  46082  fourierdlem31  46093  fourierdlem79  46140  sge0iunmptlemre  46370  ovnlerp  46517  opnvonmbllem1  46587  preimagelt  46654  preimalegt  46655  pimconstlt1  46657  pimltpnff  46658  pimrecltpos  46663  pimiooltgt  46665  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  preimageiingt  46675  preimaleiinlt  46676  pimgtmnff  46677  pimrecltneg  46679  sssmf  46693  incsmflem  46696  issmfle  46700  issmfgt  46711  smfaddlem1  46718  decsmflem  46721  issmfge  46725  smflimlem2  46727  smflim  46732  smfresal  46743  smfmullem2  46747  smfmullem4  46749  smfpimbor1lem2  46754  smflim2  46761  smfpimcclem  46762  smfsup  46769  smfinf  46773  smflimsuplem2  46776  smflimsuplem5  46779  smflimsuplem7  46781  smflimsup  46783  smfliminf  46786  smfdivdmmbl2  46796  fsupdm  46797  fsupdm2  46798  finfdm  46801  finfdm2  46802  prmdvdsfmtnof1lem1  47508