|   | 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 1780 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
| 2 | nfald.1 | . . . 4 ⊢ Ⅎ𝑦𝜑 | |
| 3 | nfald.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
| 4 | 3 | nfnd 1858 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | 
| 5 | 2, 4 | nfald 2328 | . . 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 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 |