Theorem nfrab1 3451

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 2905	. 2 ⊢ Ⅎ𝑥{𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	1, 2	nfcxfr 2901	1 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 396   ∈ wcel 2106  {cab 2709  Ⅎwnfc 2883  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rab 3433

This theorem is referenced by:  rabss3d  4078  reusv2lem4  5398  reusv2  5400  rabxfrd  5414  riotaxfrd  7396  onminsb  7778  tfis  7840  oawordeulem  8550  nnawordex  8633  rankidb  9791  tskwe  9941  cardmin2  9990  cardaleph  10080  cardmin  10555  nnwos  12895  neiptopnei  22627  dissnlocfin  23024  imasnopn  23185  imasncld  23186  imasncls  23187  blval2  24062  iundisj  25056  mbfinf  25173  sltval2  27148  lfgrnloop  28374  difrab2  31725  rabexgfGS  31726  eqrrabd  31728  iundisjf  31807  fimarab  31855  aciunf1  31875  fpwrelmap  31945  fpwrelmapffs  31946  iundisjfi  31994  locfinreflem  32808  zarcls  32842  ordtconnlem1  32892  esumrnmpt2  33054  esumpinfval  33059  hasheuni  33071  ldsysgenld  33146  measvuni  33200  eulerpartlemn  33368  ballotlem7  33522  ballotth  33524  reprdifc  33627  bnj1230  33801  bnj1476  33846  bnj1204  34011  bnj1311  34023  satfv1  34342  bj-rabtrALT  35799  topdifinfindis  36215  icorempo  36220  isbasisrelowllem1  36224  isbasisrelowllem2  36225  relowlssretop  36232  phpreu  36460  poimirlem26  36502  poimirlem27  36503  mbfposadd  36523  cover2  36571  naddwordnexlem4  42137  rababg  42310  rfcnpre1  43688  rfcnpre2  43700  ssrab2f  43791  infnsuprnmpt  43940  allbutfiinf  44116  supminfxr2  44165  pimxrneun  44185  fsumiunss  44277  limcperiod  44330  fnlimcnv  44369  fnlimfvre2  44379  fnlimf  44380  limsupequzmpt2  44420  liminfequzmpt2  44493  dvcosre  44614  stoweidlem14  44716  stoweidlem26  44728  stoweidlem31  44733  stoweidlem34  44736  stoweidlem35  44737  stoweidlem46  44748  stoweidlem50  44752  stoweidlem51  44753  stoweidlem52  44754  stoweidlem53  44755  stoweidlem54  44756  stoweidlem57  44759  stoweidlem59  44761  fourierdlem20  44829  fourierdlem31  44840  fourierdlem79  44887  sge0iunmptlemre  45117  ovnlerp  45264  opnvonmbllem1  45334  preimagelt  45401  preimalegt  45402  pimconstlt1  45404  pimltpnff  45405  pimrecltpos  45410  pimiooltgt  45412  pimdecfgtioc  45417  pimincfltioc  45418  pimdecfgtioo  45419  pimincfltioo  45420  preimageiingt  45422  preimaleiinlt  45423  pimgtmnff  45424  pimrecltneg  45426  sssmf  45440  incsmflem  45443  issmfle  45447  issmfgt  45458  smfaddlem1  45465  decsmflem  45468  issmfge  45472  smflimlem2  45474  smflim  45479  smfresal  45490  smfmullem2  45494  smfmullem4  45496  smfpimbor1lem2  45501  smflim2  45508  smfpimcclem  45509  smfsup  45516  smfinf  45520  smflimsuplem2  45523  smflimsuplem5  45526  smflimsuplem7  45528  smflimsup  45530  smfliminf  45533  smfdivdmmbl2  45543  fsupdm  45544  fsupdm2  45545  finfdm  45548  finfdm2  45549  prmdvdsfmtnof1lem1  46238