Theorem nfe1 1549

Description: 𝑥 is not free in ∃𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfe1	⊢ Ⅎ𝑥∃𝑥𝜑

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 1548	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nfi 1515	1 ⊢ Ⅎ𝑥∃𝑥𝜑

This proof depends on syntax axioms:  Ⅎwnf 1513  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie1 1546

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nf3  1721  sb4or  1886  nfmo1  2098  euexex  2172  2moswapdc  2177  nfre1  2593  ceqsexg  2954  morex  3010  sbc6g  3076  intab  3999  nfopab1  4201  nfopab2  4202  copsexg  4386  copsex2t  4387  copsex2g  4388  eusv2nf  4604  onintonm  4666  mosubopt  4842  dmcoss  5054  imadif  5464  funimaexglem  5467  nfoprab1  6140  nfoprab2  6141  nfoprab3  6142  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  dfgrp3mlem  13962