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 𝜓, 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 1781 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1858 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfald 2347 | . . 3 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ¬ 𝜓) |
6 | 5 | nfnd 1858 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓) |
7 | 1, 6 | nfxfrd 1854 | 1 ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1535 ∃wex 1780 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-11 2161 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-or 844 df-ex 1781 df-nf 1785 |
This theorem is referenced by: nfmod2 2642 nfmodv 2643 nfeudw 2677 nfeld 2991 axrepndlem1 10016 axrepndlem2 10017 axunndlem1 10019 axunnd 10020 axpowndlem2 10022 axpowndlem3 10023 axpowndlem4 10024 axregndlem2 10027 axinfndlem1 10029 axinfnd 10030 axacndlem4 10034 axacndlem5 10035 axacnd 10036 19.9d2rf 30237 hbexg 40897 |
Copyright terms: Public domain | W3C validator |