Theorem nfrab1 3431

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144  {cab 2738  Ⅎwnfc 2907  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413

This theorem is used by:  rabss3d  4006  eqrrabd  4011  reusv2lem4  5362  reusv2  5364  rabxfrd  5378  fimarab  6960  riotaxfrd  7412  onminsb  7809  tfis  7867  oawordeulem  8566  nnawordex  8650  rankidb  9812  tskwe  10035  cardmin2  10084  cardaleph  10172  cardmin  10652  nnwos  13046  rspsn0  21532  neiptopnei  23456  dissnlocfin  23854  imasnopn  24015  imasncld  24016  imasncls  24017  blval2  24887  iundisj  25875  mbfinf  25992  ltsval2  28019  lfgrnloop  29709  difrab2  33142  rabexgfGS  33143  iundisjf  33231  aciunf1  33305  fpwrelmap  33372  fpwrelmapffs  33373  iundisjfi  33435  algextdeglem6  34401  constrfin  34425  locfinreflem  34519  zarcls  34553  ordtconnlem1  34603  esumrnmpt2  34747  esumpinfval  34752  hasheuni  34764  ldsysgenld  34840  measvuni  34894  eulerpartlemn  35060  ballotlem7  35215  ballotth  35217  reprdifc  35303  bnj1230  35479  bnj1476  35524  bnj1204  35689  bnj1311  35701  onvf1odlem2  35952  onprcf1acwevdlem2  35966  vonf1oonfo  35969  onprcf1of1ord  35975  satfv1  36215  bj-rabtrALT  37937  topdifinfindis  38363  icorempo  38368  isbasisrelowllem1  38372  isbasisrelowllem2  38373  relowlssretop  38380  phpreu  38621  poimirlem26  38658  poimirlem27  38659  mbfposadd  38679  cover2  38743  naddwordnexlem4  44497  rababg  44669  permaxsep  46091  rfcnpre1  46130  rfcnpre2  46142  ssrab2f  46226  infnsuprnmpt  46356  allbutfiinf  46524  supminfxr2  46573  pimxrneun  46592  limcperiod  46734  fnlimcnv  46771  fnlimfvre2  46781  fnlimf  46782  limsupequzmpt2  46822  liminfequzmpt2  46895  dvcosre  47016  stoweidlem14  47118  stoweidlem26  47130  stoweidlem31  47135  stoweidlem34  47138  stoweidlem35  47139  stoweidlem46  47150  stoweidlem50  47154  stoweidlem51  47155  stoweidlem52  47156  stoweidlem53  47157  stoweidlem54  47158  stoweidlem57  47161  stoweidlem59  47163  fourierdlem20  47231  fourierdlem31  47242  fourierdlem79  47289  sge0iunmptlemre  47519  ovnlerp  47666  opnvonmbllem1  47736  preimagelt  47803  preimalegt  47804  pimconstlt1  47806  pimltpnff  47807  pimrecltpos  47812  pimiooltgt  47814  pimdecfgtioc  47819  pimincfltioc  47820  pimdecfgtioo  47821  pimincfltioo  47822  preimageiingt  47824  preimaleiinlt  47825  pimgtmnff  47826  pimrecltneg  47828  sssmf  47842  incsmflem  47845  issmfle  47849  issmfgt  47860  smfaddlem1  47867  decsmflem  47870  issmfge  47874  smflimlem2  47876  smflim  47881  smfresal  47892  smfmullem2  47896  smfmullem4  47898  smfpimbor1lem2  47903  smflim2  47910  smfpimcclem  47911  smfsup  47918  smfinf  47922  smflimsuplem2  47925  smflimsuplem5  47928  smflimsuplem7  47930  smflimsup  47932  smfliminf  47935  smfdivdmmbl2  47945  fsupdm  47946  fsupdm2  47947  finfdm  47950  finfdm2  47951  prmdvdsfmtnof1lem1  48763