Theorem nfrab1 3409

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  {cab 2714  Ⅎwnfc 2883  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3390

This theorem is referenced by:  rabss3d  4021  eqrrabd  4026  reusv2lem4  5343  reusv2  5345  rabxfrd  5359  fimarab  6914  riotaxfrd  7358  onminsb  7748  tfis  7806  oawordeulem  8489  nnawordex  8573  rankidb  9724  tskwe  9874  cardmin2  9923  cardaleph  10011  cardmin  10486  nnwos  12865  neiptopnei  23097  dissnlocfin  23494  imasnopn  23655  imasncld  23656  imasncls  23657  blval2  24527  iundisj  25515  mbfinf  25632  ltsval2  27620  lfgrnloop  29194  difrab2  32567  rabexgfGS  32569  iundisjf  32659  aciunf1  32736  fpwrelmap  32806  fpwrelmapffs  32807  iundisjfi  32869  algextdeglem6  33866  constrfin  33890  locfinreflem  33984  zarcls  34018  ordtconnlem1  34068  esumrnmpt2  34212  esumpinfval  34217  hasheuni  34229  ldsysgenld  34304  measvuni  34358  eulerpartlemn  34525  ballotlem7  34680  ballotth  34682  reprdifc  34771  bnj1230  34944  bnj1476  34989  bnj1204  35154  bnj1311  35166  onvf1odlem2  35286  satfv1  35545  bj-rabtrALT  37238  topdifinfindis  37662  icorempo  37667  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  phpreu  37925  poimirlem26  37967  poimirlem27  37968  mbfposadd  37988  cover2  38036  naddwordnexlem4  43829  rababg  44001  permaxsep  45434  rfcnpre1  45450  rfcnpre2  45462  ssrab2f  45547  infnsuprnmpt  45679  allbutfiinf  45848  supminfxr2  45897  pimxrneun  45916  limcperiod  46058  fnlimcnv  46095  fnlimfvre2  46105  fnlimf  46106  limsupequzmpt2  46146  liminfequzmpt2  46219  dvcosre  46340  stoweidlem14  46442  stoweidlem26  46454  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem46  46474  stoweidlem50  46478  stoweidlem51  46479  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem57  46485  stoweidlem59  46487  fourierdlem20  46555  fourierdlem31  46566  fourierdlem79  46613  sge0iunmptlemre  46843  ovnlerp  46990  opnvonmbllem1  47060  preimagelt  47127  preimalegt  47128  pimconstlt1  47130  pimltpnff  47131  pimrecltpos  47136  pimiooltgt  47138  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  pimgtmnff  47150  pimrecltneg  47152  sssmf  47166  incsmflem  47169  issmfle  47173  issmfgt  47184  smfaddlem1  47191  decsmflem  47194  issmfge  47198  smflimlem2  47200  smflim  47205  smfresal  47216  smfmullem2  47220  smfmullem4  47222  smfpimbor1lem2  47227  smflim2  47234  smfpimcclem  47235  smfsup  47242  smfinf  47246  smflimsuplem2  47249  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256  smfliminf  47259  smfdivdmmbl2  47269  fsupdm  47270  fsupdm2  47271  finfdm  47274  finfdm2  47275  prmdvdsfmtnof1lem1  48047