Theorem nfre1 3257

Description: The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfre1	⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

Proof of Theorem nfre1

Step	Hyp	Ref	Expression
1		df-rex 3057	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfe1 2153	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∧ wa 395  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2144

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-rex 3057

This theorem is referenced by:  2rmorex  3708  2reurex  3714  reuan  3842  2reu4lem  4469  nfiu1  4975  nfiu1OLD  4976  reusv2lem3  5336  fvelimad  6889  fsnex  7217  eusvobj2  7338  fiun  7875  f1iun  7876  zfregclOLD  9481  scott0  9779  ac6c4  10372  lbzbi  12834  mreiincl  17498  lss1d  20896  neiptopnei  23047  neitr  23095  utopsnneiplem  24162  cfilucfil  24474  2sqmo  27375  nosupbnd2  27655  noinfbnd2  27670  mptelee  28873  isch3  31221  atom1d  32333  opreu2reuALT  32456  iinabrex  32549  xrofsup  32750  locfinreflem  33853  esumc  34064  esumrnmpt2  34081  hasheuni  34098  esumcvg  34099  esumcvgre  34104  voliune  34242  volfiniune  34243  ddemeas  34249  eulerpartlemgvv  34389  bnj900  34941  bnj1189  35021  bnj1204  35024  bnj1398  35046  bnj1444  35055  bnj1445  35056  bnj1446  35057  bnj1447  35058  bnj1467  35066  bnj1518  35076  bnj1519  35077  iooelexlt  37404  fvineqsneq  37454  ptrest  37667  poimirlem26  37694  indexa  37781  filbcmb  37788  sdclem1  37791  heibor1  37858  dihglblem5  41345  unielss  43259  oaun3lem1  43415  suprnmpt  45219  disjinfi  45237  upbdrech  45354  ssfiunibd  45358  infxrunb2  45414  supxrunb3  45445  iccshift  45566  iooshift  45570  islpcn  45685  limsupre  45687  limclner  45697  limsupre3uzlem  45781  climuzlem  45789  xlimmnfv  45880  xlimpnfv  45884  itgperiod  46027  stoweidlem53  46099  stoweidlem57  46103  fourierdlem48  46200  fourierdlem51  46203  fourierdlem73  46225  fourierdlem81  46233  elaa2  46280  etransclem32  46312  sge0iunmptlemre  46461  voliunsge0lem  46518  meaiuninc3v  46530  isomenndlem  46576  ovnsubaddlem1  46616  hoidmvlelem1  46641  hoidmvlelem5  46645  smfaddlem1  46809  2reu7  47150  2reu8  47151  f1oresf1o2  47330  mogoldbb  47824  2zrngagrp  48288  2zrngmmgm  48291