Theorem nfe1 1484

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 1483	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nfi 1450	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  Ⅎwnf 1448  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ie1 1481

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  nf3  1657  sb4or  1821  nfmo1  2026  euexex  2099  2moswapdc  2104  nfre1  2509  ceqsexg  2854  morex  2910  sbc6g  2975  rgenm  3511  intab  3853  nfopab1  4051  nfopab2  4052  copsexg  4222  copsex2t  4223  copsex2g  4224  eusv2nf  4434  onintonm  4494  mosubopt  4669  dmcoss  4873  imadif  5268  funimaexglem  5271  nfoprab1  5891  nfoprab2  5892  nfoprab3  5893  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159