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

Theorem nfexd 2335
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 1876 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1955 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2334 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1955 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1950 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1651  wex 1875  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-10 2185  ax-11 2200  ax-12 2213
This theorem depends on definitions:  df-bi 199  df-or 875  df-ex 1876  df-nf 1880
This theorem is referenced by:  nfmod2  2602  nfeud2OLD  2639  nfeld  2948  axrepndlem1  9700  axrepndlem2  9701  axunndlem1  9703  axunnd  9704  axpowndlem2  9706  axpowndlem3  9707  axpowndlem4  9708  axregndlem2  9711  axinfndlem1  9713  axinfnd  9714  axacndlem4  9718  axacndlem5  9719  axacnd  9720  19.9d2rf  29835  hbexg  39530
  Copyright terms: Public domain W3C validator