Theorem nfe1 1496

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

Syntax hints:  Ⅎwnf 1460  ∃wex 1492

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 1449  ax-ie1 1493

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

This theorem is referenced by:  nf3  1669  sb4or  1833  nfmo1  2038  euexex  2111  2moswapdc  2116  nfre1  2520  ceqsexg  2866  morex  2922  sbc6g  2988  rgenm  3526  intab  3874  nfopab1  4073  nfopab2  4074  copsexg  4245  copsex2t  4246  copsex2g  4247  eusv2nf  4457  onintonm  4517  mosubopt  4692  dmcoss  4897  imadif  5297  funimaexglem  5300  nfoprab1  5924  nfoprab2  5925  nfoprab3  5926  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  dfgrp3mlem  12968