Theorem nfrab1 3432

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  {cab 2739  Ⅎwnfc 2908  {crab 3413

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414

This theorem is used by:  rabss3d  4029  eqrrabd  4034  reusv2lem4  5363  reusv2  5365  rabxfrd  5379  fimarab  6959  riotaxfrd  7411  onminsb  7808  tfis  7866  oawordeulem  8562  nnawordex  8646  rankidb  9808  tskwe  10031  cardmin2  10080  cardaleph  10168  cardmin  10648  nnwos  13042  rspsn0  21526  neiptopnei  23450  dissnlocfin  23848  imasnopn  24009  imasncld  24010  imasncls  24011  blval2  24881  iundisj  25869  mbfinf  25986  ltsval2  28013  lfgrnloop  29703  difrab2  33094  rabexgfGS  33095  iundisjf  33183  aciunf1  33257  fpwrelmap  33325  fpwrelmapffs  33326  iundisjfi  33388  algextdeglem6  34354  constrfin  34378  locfinreflem  34472  zarcls  34506  ordtconnlem1  34556  esumrnmpt2  34700  esumpinfval  34705  hasheuni  34717  ldsysgenld  34793  measvuni  34847  eulerpartlemn  35013  ballotlem7  35168  ballotth  35170  reprdifc  35256  bnj1230  35432  bnj1476  35477  bnj1204  35642  bnj1311  35654  onvf1odlem2  35883  onprcf1acwevdlem2  35896  vonf1oonfo  35898  satfv1  36128  bj-rabtrALT  37844  topdifinfindis  38269  icorempo  38274  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlssretop  38286  phpreu  38527  poimirlem26  38564  poimirlem27  38565  mbfposadd  38585  cover2  38649  naddwordnexlem4  44402  rababg  44574  permaxsep  45996  rfcnpre1  46035  rfcnpre2  46047  ssrab2f  46131  infnsuprnmpt  46261  allbutfiinf  46429  supminfxr2  46478  pimxrneun  46497  limcperiod  46639  fnlimcnv  46676  fnlimfvre2  46686  fnlimf  46687  limsupequzmpt2  46727  liminfequzmpt2  46800  dvcosre  46921  stoweidlem14  47023  stoweidlem26  47035  stoweidlem31  47040  stoweidlem34  47043  stoweidlem35  47044  stoweidlem46  47055  stoweidlem50  47059  stoweidlem51  47060  stoweidlem52  47061  stoweidlem53  47062  stoweidlem54  47063  stoweidlem57  47066  stoweidlem59  47068  fourierdlem20  47136  fourierdlem31  47147  fourierdlem79  47194  sge0iunmptlemre  47424  ovnlerp  47571  opnvonmbllem1  47641  preimagelt  47708  preimalegt  47709  pimconstlt1  47711  pimltpnff  47712  pimrecltpos  47717  pimiooltgt  47719  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  preimageiingt  47729  preimaleiinlt  47730  pimgtmnff  47731  pimrecltneg  47733  sssmf  47747  incsmflem  47750  issmfle  47754  issmfgt  47765  smfaddlem1  47772  decsmflem  47775  issmfge  47779  smflimlem2  47781  smflim  47786  smfresal  47797  smfmullem2  47801  smfmullem4  47803  smfpimbor1lem2  47808  smflim2  47815  smfpimcclem  47816  smfsup  47823  smfinf  47827  smflimsuplem2  47830  smflimsuplem5  47833  smflimsuplem7  47835  smflimsup  47837  smfliminf  47840  smfdivdmmbl2  47850  fsupdm  47851  fsupdm2  47852  finfdm  47855  finfdm2  47856  prmdvdsfmtnof1lem1  48668