Theorem nfrab1 3464

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  {cab 2717  Ⅎwnfc 2893  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rab 3444

This theorem is referenced by:  rabss3d  4104  eqrrabd  4109  reusv2lem4  5419  reusv2  5421  rabxfrd  5435  fimarab  6996  riotaxfrd  7439  onminsb  7830  tfis  7892  oawordeulem  8610  nnawordex  8693  rankidb  9869  tskwe  10019  cardmin2  10068  cardaleph  10158  cardmin  10633  nnwos  12980  neiptopnei  23161  dissnlocfin  23558  imasnopn  23719  imasncld  23720  imasncls  23721  blval2  24596  iundisj  25602  mbfinf  25719  sltval2  27719  lfgrnloop  29160  difrab2  32526  rabexgfGS  32527  iundisjf  32611  aciunf1  32681  fpwrelmap  32747  fpwrelmapffs  32748  iundisjfi  32801  algextdeglem6  33713  constrfin  33736  locfinreflem  33786  zarcls  33820  ordtconnlem1  33870  esumrnmpt2  34032  esumpinfval  34037  hasheuni  34049  ldsysgenld  34124  measvuni  34178  eulerpartlemn  34346  ballotlem7  34500  ballotth  34502  reprdifc  34604  bnj1230  34778  bnj1476  34823  bnj1204  34988  bnj1311  35000  satfv1  35331  bj-rabtrALT  36897  topdifinfindis  37312  icorempo  37317  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  phpreu  37564  poimirlem26  37606  poimirlem27  37607  mbfposadd  37627  cover2  37675  naddwordnexlem4  43363  rababg  43536  rfcnpre1  44919  rfcnpre2  44931  ssrab2f  45019  infnsuprnmpt  45159  allbutfiinf  45335  supminfxr2  45384  pimxrneun  45404  limcperiod  45549  fnlimcnv  45588  fnlimfvre2  45598  fnlimf  45599  limsupequzmpt2  45639  liminfequzmpt2  45712  dvcosre  45833  stoweidlem14  45935  stoweidlem26  45947  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem46  45967  stoweidlem50  45971  stoweidlem51  45972  stoweidlem52  45973  stoweidlem53  45974  stoweidlem54  45975  stoweidlem57  45978  stoweidlem59  45980  fourierdlem20  46048  fourierdlem31  46059  fourierdlem79  46106  sge0iunmptlemre  46336  ovnlerp  46483  opnvonmbllem1  46553  preimagelt  46620  preimalegt  46621  pimconstlt1  46623  pimltpnff  46624  pimrecltpos  46629  pimiooltgt  46631  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  pimgtmnff  46643  pimrecltneg  46645  sssmf  46659  incsmflem  46662  issmfle  46666  issmfgt  46677  smfaddlem1  46684  decsmflem  46687  issmfge  46691  smflimlem2  46693  smflim  46698  smfresal  46709  smfmullem2  46713  smfmullem4  46715  smfpimbor1lem2  46720  smflim2  46727  smfpimcclem  46728  smfsup  46735  smfinf  46739  smflimsuplem2  46742  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749  smfliminf  46752  smfdivdmmbl2  46762  fsupdm  46763  fsupdm2  46764  finfdm  46767  finfdm2  46768  prmdvdsfmtnof1lem1  47458