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

Theorem nfexd 2166
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 1704 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1784 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2164 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1784 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1779 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1480  wex 1703  wnf 1707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-10 2018  ax-11 2033  ax-12 2046
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1704  df-nf 1709
This theorem is referenced by:  nfeud2  2481  nfeld  2772  axrepndlem1  9411  axrepndlem2  9412  axunndlem1  9414  axunnd  9415  axpowndlem2  9417  axpowndlem3  9418  axpowndlem4  9419  axregndlem2  9422  axinfndlem1  9424  axinfnd  9425  axacndlem4  9429  axacndlem5  9430  axacnd  9431  19.9d2rf  29302  hbexg  38598
  Copyright terms: Public domain W3C validator