Theorem nfe1 1518

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

Syntax hints:  Ⅎwnf 1482  ∃wex 1514

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 1471  ax-ie1 1515

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

This theorem is referenced by:  nf3  1691  sb4or  1855  nfmo1  2065  euexex  2138  2moswapdc  2143  nfre1  2548  ceqsexg  2900  morex  2956  sbc6g  3022  intab  3913  nfopab1  4112  nfopab2  4113  copsexg  4287  copsex2t  4288  copsex2g  4289  eusv2nf  4502  onintonm  4564  mosubopt  4739  dmcoss  4947  imadif  5353  funimaexglem  5356  nfoprab1  5993  nfoprab2  5994  nfoprab3  5995  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  dfgrp3mlem  13372