![]() |
Mathbox for Steven Nguyen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sn-el | Structured version Visualization version GIF version |
Description: A version of el 5235 with an inner existential quantifier on 𝑥, which avoids ax-7 2015 and ax-8 2113. (Contributed by SN, 18-Sep-2023.) |
Ref | Expression |
---|---|
sn-el | ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-pow 5231 | . 2 ⊢ ∃𝑦∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) | |
2 | ax6ev 1972 | . . . 4 ⊢ ∃𝑥 𝑥 = 𝑧 | |
3 | ax9v1 2123 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) | |
4 | 3 | alrimiv 1928 | . . . 4 ⊢ (𝑥 = 𝑧 → ∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧)) |
5 | 2, 4 | eximii 1838 | . . 3 ⊢ ∃𝑥∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) |
6 | exim 1835 | . . 3 ⊢ (∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) → (∃𝑥∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → ∃𝑥 𝑥 ∈ 𝑦)) | |
7 | 5, 6 | mpi 20 | . 2 ⊢ (∀𝑥(∀𝑤(𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧) → 𝑥 ∈ 𝑦) → ∃𝑥 𝑥 ∈ 𝑦) |
8 | 1, 7 | eximii 1838 | 1 ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 ∃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 1911 ax-6 1970 ax-9 2121 ax-pow 5231 |
This theorem depends on definitions: df-bi 210 df-ex 1782 |
This theorem is referenced by: sn-dtru 39403 |
Copyright terms: Public domain | W3C validator |