Theorem nfrab1 3457

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  {cab 2714  Ⅎwnfc 2890  {crab 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437

This theorem is referenced by:  rabss3d  4081  eqrrabd  4086  reusv2lem4  5401  reusv2  5403  rabxfrd  5417  fimarab  6983  riotaxfrd  7422  onminsb  7814  tfis  7876  oawordeulem  8592  nnawordex  8675  rankidb  9840  tskwe  9990  cardmin2  10039  cardaleph  10129  cardmin  10604  nnwos  12957  neiptopnei  23140  dissnlocfin  23537  imasnopn  23698  imasncld  23699  imasncls  23700  blval2  24575  iundisj  25583  mbfinf  25700  sltval2  27701  lfgrnloop  29142  difrab2  32517  rabexgfGS  32518  iundisjf  32602  aciunf1  32673  fpwrelmap  32744  fpwrelmapffs  32745  iundisjfi  32798  algextdeglem6  33763  constrfin  33787  locfinreflem  33839  zarcls  33873  ordtconnlem1  33923  esumrnmpt2  34069  esumpinfval  34074  hasheuni  34086  ldsysgenld  34161  measvuni  34215  eulerpartlemn  34383  ballotlem7  34538  ballotth  34540  reprdifc  34642  bnj1230  34816  bnj1476  34861  bnj1204  35026  bnj1311  35038  satfv1  35368  bj-rabtrALT  36932  topdifinfindis  37347  icorempo  37352  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  phpreu  37611  poimirlem26  37653  poimirlem27  37654  mbfposadd  37674  cover2  37722  naddwordnexlem4  43414  rababg  43587  rfcnpre1  45024  rfcnpre2  45036  ssrab2f  45122  infnsuprnmpt  45257  allbutfiinf  45431  supminfxr2  45480  pimxrneun  45499  limcperiod  45643  fnlimcnv  45682  fnlimfvre2  45692  fnlimf  45693  limsupequzmpt2  45733  liminfequzmpt2  45806  dvcosre  45927  stoweidlem14  46029  stoweidlem26  46041  stoweidlem31  46046  stoweidlem34  46049  stoweidlem35  46050  stoweidlem46  46061  stoweidlem50  46065  stoweidlem51  46066  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  stoweidlem57  46072  stoweidlem59  46074  fourierdlem20  46142  fourierdlem31  46153  fourierdlem79  46200  sge0iunmptlemre  46430  ovnlerp  46577  opnvonmbllem1  46647  preimagelt  46714  preimalegt  46715  pimconstlt1  46717  pimltpnff  46718  pimrecltpos  46723  pimiooltgt  46725  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  preimageiingt  46735  preimaleiinlt  46736  pimgtmnff  46737  pimrecltneg  46739  sssmf  46753  incsmflem  46756  issmfle  46760  issmfgt  46771  smfaddlem1  46778  decsmflem  46781  issmfge  46785  smflimlem2  46787  smflim  46792  smfresal  46803  smfmullem2  46807  smfmullem4  46809  smfpimbor1lem2  46814  smflim2  46821  smfpimcclem  46822  smfsup  46829  smfinf  46833  smflimsuplem2  46836  smflimsuplem5  46839  smflimsuplem7  46841  smflimsup  46843  smfliminf  46846  smfdivdmmbl2  46856  fsupdm  46857  fsupdm2  46858  finfdm  46861  finfdm2  46862  prmdvdsfmtnof1lem1  47571