![]() |
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 1774 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfnd 1853 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
5 | 2, 4 | nfald 2316 | . . 3 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ¬ 𝜓) |
6 | 5 | nfnd 1853 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜓) |
7 | 1, 6 | nfxfrd 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 |