Theorem nfre1 3308

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 3146	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfe1 2154	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1853	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∧ wa 398  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2114  ∃wrex 3141

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 2145

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785  df-rex 3146

This theorem is referenced by:  r19.29anOLD  3334  2rmorex  3747  2reurex  3752  reuan  3882  2reu4lem  4467  nfiu1  4955  reusv2lem3  5303  fvelimad  6734  fsnex  7041  eusvobj2  7151  fiun  7646  f1iun  7647  zfregcl  9060  scott0  9317  ac6c4  9905  lbzbi  12339  mreiincl  16869  lss1d  19737  neiptopnei  21742  neitr  21790  utopsnneiplem  22858  cfilucfil  23171  2sqmo  26015  mptelee  26683  isch3  29020  atom1d  30132  opreu2reuALT  30242  xrofsup  30494  locfinreflem  31106  esumc  31312  esumrnmpt2  31329  hasheuni  31346  esumcvg  31347  esumcvgre  31352  voliune  31490  volfiniune  31491  ddemeas  31497  eulerpartlemgvv  31636  bnj900  32203  bnj1189  32283  bnj1204  32286  bnj1398  32308  bnj1444  32317  bnj1445  32318  bnj1446  32319  bnj1447  32320  bnj1467  32328  bnj1518  32338  bnj1519  32339  nosupbnd2  33218  iooelexlt  34645  fvineqsneq  34695  ptrest  34893  poimirlem26  34920  indexa  35010  filbcmb  35017  sdclem1  35020  heibor1  35090  dihglblem5  38436  suprnmpt  41437  disjinfi  41461  upbdrech  41579  ssfiunibd  41583  infxrunb2  41643  supxrunb3  41679  iccshift  41801  iooshift  41805  islpcn  41927  limsupre  41929  limclner  41939  limsupre3uzlem  42023  climuzlem  42031  xlimmnfv  42122  xlimpnfv  42126  itgperiod  42273  stoweidlem53  42345  stoweidlem57  42349  fourierdlem48  42446  fourierdlem51  42449  fourierdlem73  42471  fourierdlem81  42479  elaa2  42526  etransclem32  42558  sge0iunmptlemre  42704  voliunsge0lem  42761  meaiuninc3v  42773  isomenndlem  42819  ovnsubaddlem1  42859  hoidmvlelem1  42884  hoidmvlelem5  42888  smfaddlem1  43046  2reu7  43317  2reu8  43318  f1oresf1o2  43497  mogoldbb  43957  2zrngagrp  44221  2zrngmmgm  44224