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 2145  {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 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413

This theorem is used by:  rabss3d  4029  eqrrabd  4034  reusv2lem4  5366  reusv2  5368  rabxfrd  5382  fimarab  6952  riotaxfrd  7404  onminsb  7793  tfis  7851  oawordeulem  8541  nnawordex  8625  rankidb  9782  tskwe  9955  cardmin2  10004  cardaleph  10092  cardmin  10572  nnwos  12964  rspsn0  21435  neiptopnei  23357  dissnlocfin  23755  imasnopn  23916  imasncld  23917  imasncls  23918  blval2  24788  iundisj  25776  mbfinf  25893  ltsval2  27892  lfgrnloop  29582  difrab2  32973  rabexgfGS  32974  iundisjf  33062  aciunf1  33136  fpwrelmap  33204  fpwrelmapffs  33205  iundisjfi  33267  algextdeglem6  34232  constrfin  34256  locfinreflem  34350  zarcls  34384  ordtconnlem1  34434  esumrnmpt2  34578  esumpinfval  34583  hasheuni  34595  ldsysgenld  34671  measvuni  34725  eulerpartlemn  34892  ballotlem7  35047  ballotth  35049  reprdifc  35135  bnj1230  35311  bnj1476  35356  bnj1204  35521  bnj1311  35533  onvf1odlem2  35701  vonf1oonfo  35712  satfv1  35942  bj-rabtrALT  37675  topdifinfindis  38100  icorempo  38105  isbasisrelowllem1  38109  isbasisrelowllem2  38110  relowlssretop  38117  phpreu  38358  poimirlem26  38395  poimirlem27  38396  mbfposadd  38416  cover2  38465  naddwordnexlem4  44242  rababg  44414  permaxsep  45830  rfcnpre1  45853  rfcnpre2  45865  ssrab2f  45949  infnsuprnmpt  46079  allbutfiinf  46248  supminfxr2  46297  pimxrneun  46316  limcperiod  46458  fnlimcnv  46495  fnlimfvre2  46505  fnlimf  46506  limsupequzmpt2  46546  liminfequzmpt2  46619  dvcosre  46740  stoweidlem14  46842  stoweidlem26  46854  stoweidlem31  46859  stoweidlem34  46862  stoweidlem35  46863  stoweidlem46  46874  stoweidlem50  46878  stoweidlem51  46879  stoweidlem52  46880  stoweidlem53  46881  stoweidlem54  46882  stoweidlem57  46885  stoweidlem59  46887  fourierdlem20  46955  fourierdlem31  46966  fourierdlem79  47013  sge0iunmptlemre  47243  ovnlerp  47390  opnvonmbllem1  47460  preimagelt  47527  preimalegt  47528  pimconstlt1  47530  pimltpnff  47531  pimrecltpos  47536  pimiooltgt  47538  pimdecfgtioc  47543  pimincfltioc  47544  pimdecfgtioo  47545  pimincfltioo  47546  preimageiingt  47548  preimaleiinlt  47549  pimgtmnff  47550  pimrecltneg  47552  sssmf  47566  incsmflem  47569  issmfle  47573  issmfgt  47584  smfaddlem1  47591  decsmflem  47594  issmfge  47598  smflimlem2  47600  smflim  47605  smfresal  47616  smfmullem2  47620  smfmullem4  47622  smfpimbor1lem2  47627  smflim2  47634  smfpimcclem  47635  smfsup  47642  smfinf  47646  smflimsuplem2  47649  smflimsuplem5  47652  smflimsuplem7  47654  smflimsup  47656  smfliminf  47659  smfdivdmmbl2  47669  fsupdm  47670  fsupdm2  47671  finfdm  47674  finfdm2  47675  prmdvdsfmtnof1lem1  48487