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  1881  nfmo1  2091  euexex  2165  2moswapdc  2170  nfre1  2576  ceqsexg  2935  morex  2991  sbc6g  3057  intab  3962  nfopab1  4163  nfopab2  4164  copsexg  4342  copsex2t  4343  copsex2g  4344  eusv2nf  4559  onintonm  4621  mosubopt  4797  dmcoss  5008  imadif  5417  funimaexglem  5420  nfoprab1  6080  nfoprab2  6081  nfoprab3  6082  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  dfgrp3mlem  13744