Theorem nfe1 1545

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

Syntax hints:  Ⅎwnf 1509  ∃wex 1541

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 1498  ax-ie1 1542

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

This theorem is referenced by:  nf3  1717  sb4or  1882  nfmo1  2094  euexex  2168  2moswapdc  2173  nfre1  2587  ceqsexg  2948  morex  3004  sbc6g  3070  intab  3983  nfopab1  4184  nfopab2  4185  copsexg  4365  copsex2t  4366  copsex2g  4367  eusv2nf  4582  onintonm  4644  mosubopt  4820  dmcoss  5032  imadif  5441  funimaexglem  5444  nfoprab1  6110  nfoprab2  6111  nfoprab3  6112  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  dfgrp3mlem  13853