![]() |
Mathbox for Steven Nguyen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sn-exelALT | Structured version Visualization version GIF version |
Description: Alternate proof of exel 5390, avoiding ax-pr 5384 but requiring ax-5 1913, ax-9 2116, and ax-pow 5320. This is similar to how elALT2 5324 uses ax-pow 5320 instead of ax-pr 5384 compared to el 5394. (Contributed by SN, 18-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sn-exelALT | ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-pow 5320 | . 2 ⊢ ∃𝑦∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) | |
2 | ax6ev 1973 | . . . 4 ⊢ ∃𝑥 𝑥 = 𝑧 | |
3 | ax9v1 2118 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) | |
4 | 3 | alrimiv 1930 | . . . 4 ⊢ (𝑥 = 𝑧 → ∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) |
5 | 2, 4 | eximii 1839 | . . 3 ⊢ ∃𝑥∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) |
6 | exim 1836 | . . 3 ⊢ (∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) → (∃𝑥∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → ∃𝑥 𝑥 ∈ 𝑦)) | |
7 | 5, 6 | mpi 20 | . 2 ⊢ (∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) → ∃𝑥 𝑥 ∈ 𝑦) |
8 | 1, 7 | eximii 1839 | 1 ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ∃wex 1781 |
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-9 2116 ax-pow 5320 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |