Theorem nfrab1 3438

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  {cab 2743  Ⅎwnfc 2912  {crab 3418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3419

This theorem is used by:  rabss3d  4036  eqrrabd  4041  reusv2lem4  5374  reusv2  5376  rabxfrd  5390  fimarab  6959  riotaxfrd  7407  onminsb  7795  tfis  7853  oawordeulem  8541  nnawordex  8625  rankidb  9775  tskwe  9948  cardmin2  9997  cardaleph  10085  cardmin  10559  nnwos  12950  rspsn0  21401  neiptopnei  23318  dissnlocfin  23715  imasnopn  23876  imasncld  23877  imasncls  23878  blval2  24748  iundisj  25736  mbfinf  25853  ltsval2  27849  lfgrnloop  29504  difrab2  32873  rabexgfGS  32874  iundisjf  32963  aciunf1  33037  fpwrelmap  33107  fpwrelmapffs  33108  iundisjfi  33170  algextdeglem6  34135  constrfin  34159  locfinreflem  34253  zarcls  34287  ordtconnlem1  34337  esumrnmpt2  34481  esumpinfval  34486  hasheuni  34498  ldsysgenld  34574  measvuni  34628  eulerpartlemn  34795  ballotlem7  34950  ballotth  34952  reprdifc  35038  bnj1230  35214  bnj1476  35259  bnj1204  35424  bnj1311  35436  onvf1odlem2  35604  vonf1oonfo  35615  satfv1  35868  bj-rabtrALT  37600  topdifinfindis  38025  icorempo  38030  isbasisrelowllem1  38034  isbasisrelowllem2  38035  relowlssretop  38042  phpreu  38288  poimirlem26  38330  poimirlem27  38331  mbfposadd  38351  cover2  38399  naddwordnexlem4  44161  rababg  44333  permaxsep  45749  rfcnpre1  45772  rfcnpre2  45784  ssrab2f  45868  infnsuprnmpt  45998  allbutfiinf  46167  supminfxr2  46216  pimxrneun  46235  limcperiod  46377  fnlimcnv  46414  fnlimfvre2  46424  fnlimf  46425  limsupequzmpt2  46465  liminfequzmpt2  46538  dvcosre  46659  stoweidlem14  46761  stoweidlem26  46773  stoweidlem31  46778  stoweidlem34  46781  stoweidlem35  46782  stoweidlem46  46793  stoweidlem50  46797  stoweidlem51  46798  stoweidlem52  46799  stoweidlem53  46800  stoweidlem54  46801  stoweidlem57  46804  stoweidlem59  46806  fourierdlem20  46874  fourierdlem31  46885  fourierdlem79  46932  sge0iunmptlemre  47162  ovnlerp  47309  opnvonmbllem1  47379  preimagelt  47446  preimalegt  47447  pimconstlt1  47449  pimltpnff  47450  pimrecltpos  47455  pimiooltgt  47457  pimdecfgtioc  47462  pimincfltioc  47463  pimdecfgtioo  47464  pimincfltioo  47465  preimageiingt  47467  preimaleiinlt  47468  pimgtmnff  47469  pimrecltneg  47471  sssmf  47485  incsmflem  47488  issmfle  47492  issmfgt  47503  smfaddlem1  47510  decsmflem  47513  issmfge  47517  smflimlem2  47519  smflim  47524  smfresal  47535  smfmullem2  47539  smfmullem4  47541  smfpimbor1lem2  47546  smflim2  47553  smfpimcclem  47554  smfsup  47561  smfinf  47565  smflimsuplem2  47568  smflimsuplem5  47571  smflimsuplem7  47573  smflimsup  47575  smfliminf  47578  smfdivdmmbl2  47588  fsupdm  47589  fsupdm2  47590  finfdm  47593  finfdm2  47594  prmdvdsfmtnof1lem1  48369