Theorem nfrab1 3419

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113  {cab 2714  Ⅎwnfc 2883  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400

This theorem is referenced by:  rabss3d  4033  eqrrabd  4038  reusv2lem4  5346  reusv2  5348  rabxfrd  5362  fimarab  6908  riotaxfrd  7349  onminsb  7739  tfis  7797  oawordeulem  8481  nnawordex  8565  rankidb  9712  tskwe  9862  cardmin2  9911  cardaleph  9999  cardmin  10474  nnwos  12828  neiptopnei  23076  dissnlocfin  23473  imasnopn  23634  imasncld  23635  imasncls  23636  blval2  24506  iundisj  25505  mbfinf  25622  ltsval2  27624  lfgrnloop  29198  difrab2  32572  rabexgfGS  32574  iundisjf  32664  aciunf1  32741  fpwrelmap  32812  fpwrelmapffs  32813  iundisjfi  32876  algextdeglem6  33879  constrfin  33903  locfinreflem  33997  zarcls  34031  ordtconnlem1  34081  esumrnmpt2  34225  esumpinfval  34230  hasheuni  34242  ldsysgenld  34317  measvuni  34371  eulerpartlemn  34538  ballotlem7  34693  ballotth  34695  reprdifc  34784  bnj1230  34958  bnj1476  35003  bnj1204  35168  bnj1311  35180  onvf1odlem2  35298  satfv1  35557  bj-rabtrALT  37132  topdifinfindis  37551  icorempo  37556  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlssretop  37568  phpreu  37805  poimirlem26  37847  poimirlem27  37848  mbfposadd  37868  cover2  37916  naddwordnexlem4  43643  rababg  43815  permaxsep  45248  rfcnpre1  45264  rfcnpre2  45276  ssrab2f  45361  infnsuprnmpt  45494  allbutfiinf  45664  supminfxr2  45713  pimxrneun  45732  limcperiod  45874  fnlimcnv  45911  fnlimfvre2  45921  fnlimf  45922  limsupequzmpt2  45962  liminfequzmpt2  46035  dvcosre  46156  stoweidlem14  46258  stoweidlem26  46270  stoweidlem31  46275  stoweidlem34  46278  stoweidlem35  46279  stoweidlem46  46290  stoweidlem50  46294  stoweidlem51  46295  stoweidlem52  46296  stoweidlem53  46297  stoweidlem54  46298  stoweidlem57  46301  stoweidlem59  46303  fourierdlem20  46371  fourierdlem31  46382  fourierdlem79  46429  sge0iunmptlemre  46659  ovnlerp  46806  opnvonmbllem1  46876  preimagelt  46943  preimalegt  46944  pimconstlt1  46946  pimltpnff  46947  pimrecltpos  46952  pimiooltgt  46954  pimdecfgtioc  46959  pimincfltioc  46960  pimdecfgtioo  46961  pimincfltioo  46962  preimageiingt  46964  preimaleiinlt  46965  pimgtmnff  46966  pimrecltneg  46968  sssmf  46982  incsmflem  46985  issmfle  46989  issmfgt  47000  smfaddlem1  47007  decsmflem  47010  issmfge  47014  smflimlem2  47016  smflim  47021  smfresal  47032  smfmullem2  47036  smfmullem4  47038  smfpimbor1lem2  47043  smflim2  47050  smfpimcclem  47051  smfsup  47058  smfinf  47062  smflimsuplem2  47065  smflimsuplem5  47068  smflimsuplem7  47070  smflimsup  47072  smfliminf  47075  smfdivdmmbl2  47085  fsupdm  47086  fsupdm2  47087  finfdm  47090  finfdm2  47091  prmdvdsfmtnof1lem1  47830