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

Theorem nfexd 2323
Description: If 𝑥 is not free in 𝜓, then 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 1783 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1862 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2322 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1862 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1857 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540  wex 1782  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787
This theorem is referenced by:  nfmod2  2553  nfmodv  2554  nfeudw  2586  nfeld  2915  nfopabd  5217  nfttrcld  9705  axrepndlem1  10587  axrepndlem2  10588  axunndlem1  10590  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  19.9d2rf  31711  hbexg  43317
  Copyright terms: Public domain W3C validator