![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfexd | Structured version Visualization version GIF version |
Description: If 𝑥 is not free in 𝜓, then it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfald.1 | ⊢ Ⅎ𝑦𝜑 |
nfald.2 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfexd | ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex 1782 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1861 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfald 2321 | . . 3 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ¬ 𝜓) |
6 | 5 | nfnd 1861 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓) |
7 | 1, 6 | nfxfrd 1856 | 1 ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1539 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-10 2137 ax-11 2154 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfmod2 2552 nfmodv 2553 nfeudw 2585 nfeld 2914 nfopabd 5216 nfttrcld 9704 axrepndlem1 10586 axrepndlem2 10587 axunndlem1 10589 axunnd 10590 axpowndlem2 10592 axpowndlem3 10593 axpowndlem4 10594 axregndlem2 10597 axinfndlem1 10599 axinfnd 10600 axacndlem4 10604 axacndlem5 10605 axacnd 10606 19.9d2rf 31706 hbexg 43307 |
Copyright terms: Public domain | W3C validator |