Theorem nfrab1 3423

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  {crab 3402

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403

This theorem is referenced by:  rabss3d  4040  eqrrabd  4045  reusv2lem4  5351  reusv2  5353  rabxfrd  5367  fimarab  6917  riotaxfrd  7360  onminsb  7750  tfis  7811  oawordeulem  8495  nnawordex  8578  rankidb  9729  tskwe  9879  cardmin2  9928  cardaleph  10018  cardmin  10493  nnwos  12850  neiptopnei  22995  dissnlocfin  23392  imasnopn  23553  imasncld  23554  imasncls  23555  blval2  24426  iundisj  25425  mbfinf  25542  sltval2  27544  lfgrnloop  29028  difrab2  32400  rabexgfGS  32401  iundisjf  32491  aciunf1  32560  fpwrelmap  32629  fpwrelmapffs  32630  iundisjfi  32692  algextdeglem6  33685  constrfin  33709  locfinreflem  33803  zarcls  33837  ordtconnlem1  33887  esumrnmpt2  34031  esumpinfval  34036  hasheuni  34048  ldsysgenld  34123  measvuni  34177  eulerpartlemn  34345  ballotlem7  34500  ballotth  34502  reprdifc  34591  bnj1230  34765  bnj1476  34810  bnj1204  34975  bnj1311  34987  onvf1odlem2  35064  satfv1  35323  bj-rabtrALT  36892  topdifinfindis  37307  icorempo  37312  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlssretop  37324  phpreu  37571  poimirlem26  37613  poimirlem27  37614  mbfposadd  37634  cover2  37682  naddwordnexlem4  43363  rababg  43536  permaxsep  44970  rfcnpre1  44986  rfcnpre2  44998  ssrab2f  45084  infnsuprnmpt  45217  allbutfiinf  45389  supminfxr2  45438  pimxrneun  45457  limcperiod  45599  fnlimcnv  45638  fnlimfvre2  45648  fnlimf  45649  limsupequzmpt2  45689  liminfequzmpt2  45762  dvcosre  45883  stoweidlem14  45985  stoweidlem26  45997  stoweidlem31  46002  stoweidlem34  46005  stoweidlem35  46006  stoweidlem46  46017  stoweidlem50  46021  stoweidlem51  46022  stoweidlem52  46023  stoweidlem53  46024  stoweidlem54  46025  stoweidlem57  46028  stoweidlem59  46030  fourierdlem20  46098  fourierdlem31  46109  fourierdlem79  46156  sge0iunmptlemre  46386  ovnlerp  46533  opnvonmbllem1  46603  preimagelt  46670  preimalegt  46671  pimconstlt1  46673  pimltpnff  46674  pimrecltpos  46679  pimiooltgt  46681  pimdecfgtioc  46686  pimincfltioc  46687  pimdecfgtioo  46688  pimincfltioo  46689  preimageiingt  46691  preimaleiinlt  46692  pimgtmnff  46693  pimrecltneg  46695  sssmf  46709  incsmflem  46712  issmfle  46716  issmfgt  46727  smfaddlem1  46734  decsmflem  46737  issmfge  46741  smflimlem2  46743  smflim  46748  smfresal  46759  smfmullem2  46763  smfmullem4  46765  smfpimbor1lem2  46770  smflim2  46777  smfpimcclem  46778  smfsup  46785  smfinf  46789  smflimsuplem2  46792  smflimsuplem5  46795  smflimsuplem7  46797  smflimsup  46799  smfliminf  46802  smfdivdmmbl2  46812  fsupdm  46813  fsupdm2  46814  finfdm  46817  finfdm2  46818  prmdvdsfmtnof1lem1  47558