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

Theorem nfexd 2329
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 1780 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1858 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfald 2328 . . 3 (𝜑 → Ⅎ𝑥𝑦 ¬ 𝜓)
65nfnd 1858 . 2 (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓)
71, 6nfxfrd 1854 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1538  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfmod2  2558  nfmodv  2559  nfeudw  2591  nfeld  2917  nfopabd  5211  nfttrcld  9750  axrepndlem1  10632  axrepndlem2  10633  axunndlem1  10635  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  19.9d2rf  32488  hbexg  44576
  Copyright terms: Public domain W3C validator