Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfexd Structured version   Visualization version   GIF version

Theorem nfexd 2350
 Description: If 𝑥 is not free in 𝜓, it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfald.1 𝑦𝜑
nfald.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfexd (𝜑 → Ⅎ𝑥𝑦𝜓)

Proof of Theorem nfexd
StepHypRef Expression
1 df-ex 1782 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1859 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2349 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1859 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1855 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786 This theorem is referenced by:  nfmod2  2643  nfmodv  2644  nfeudw  2678  nfeld  2993  axrepndlem1  10014  axrepndlem2  10015  axunndlem1  10017  axunnd  10018  axpowndlem2  10020  axpowndlem3  10021  axpowndlem4  10022  axregndlem2  10025  axinfndlem1  10027  axinfnd  10028  axacndlem4  10032  axacndlem5  10033  axacnd  10034  19.9d2rf  30251  hbexg  41210
 Copyright terms: Public domain W3C validator