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  6069  nfoprab2  6070  nfoprab3  6071  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  dfgrp3mlem  13680