Theorem nfe1 1544

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

Syntax hints:  Ⅎwnf 1508  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1497  ax-ie1 1541

This theorem depends on definitions:  df-bi 117  df-nf 1509

This theorem is referenced by:  nf3  1717  sb4or  1881  nfmo1  2091  euexex  2165  2moswapdc  2170  nfre1  2575  ceqsexg  2934  morex  2990  sbc6g  3056  intab  3957  nfopab1  4158  nfopab2  4159  copsexg  4336  copsex2t  4337  copsex2g  4338  eusv2nf  4553  onintonm  4615  mosubopt  4791  dmcoss  5002  imadif  5410  funimaexglem  5413  nfoprab1  6070  nfoprab2  6071  nfoprab3  6072  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  dfgrp3mlem  13686