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 1777 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1854 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfald 2343 | . . 3 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ¬ 𝜓) |
6 | 5 | nfnd 1854 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓) |
7 | 1, 6 | nfxfrd 1850 | 1 ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1531 ∃wex 1776 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-10 2141 ax-11 2157 ax-12 2173 |
This theorem depends on definitions: df-bi 209 df-or 844 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nfmod2 2638 nfmodv 2639 nfeudw 2673 nfeld 2989 axrepndlem1 10008 axrepndlem2 10009 axunndlem1 10011 axunnd 10012 axpowndlem2 10014 axpowndlem3 10015 axpowndlem4 10016 axregndlem2 10019 axinfndlem1 10021 axinfnd 10022 axacndlem4 10026 axacndlem5 10027 axacnd 10028 19.9d2rf 30229 hbexg 40883 |
Copyright terms: Public domain | W3C validator |