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

Theorem nfexd 2317
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 1774 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1853 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2316 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1853 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1848 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1531  wex 1773  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1774  df-nf 1778
This theorem is referenced by:  nfmod2  2546  nfmodv  2547  nfeudw  2579  nfeld  2903  nfopabd  5220  nfttrcld  9749  axrepndlem1  10631  axrepndlem2  10632  axunndlem1  10634  axunnd  10635  axpowndlem2  10637  axpowndlem3  10638  axpowndlem4  10639  axregndlem2  10642  axinfndlem1  10644  axinfnd  10645  axacndlem4  10649  axacndlem5  10650  axacnd  10651  19.9d2rf  32390  hbexg  44169
  Copyright terms: Public domain W3C validator