| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exel | Structured version Visualization version GIF version | ||
| Description: There exist two sets, one
a member of the other.
This theorem looks similar to el 5442, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1809, ax-6 1967, and ax-pr 5432. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5439. (Contributed by SN, 23-Dec-2024.) |
| Ref | Expression |
|---|---|
| exel | ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-pr 5432 | . 2 ⊢ ∃𝑦∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦) | |
| 2 | ax6ev 1969 | . . . 4 ⊢ ∃𝑥 𝑥 = 𝑧 | |
| 3 | pm2.07 903 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑧 ∨ 𝑥 = 𝑧)) | |
| 4 | 2, 3 | eximii 1837 | . . 3 ⊢ ∃𝑥(𝑥 = 𝑧 ∨ 𝑥 = 𝑧) |
| 5 | exim 1834 | . . 3 ⊢ (∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦) → (∃𝑥(𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → ∃𝑥 𝑥 ∈ 𝑦)) | |
| 6 | 4, 5 | mpi 20 | . 2 ⊢ (∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦) → ∃𝑥 𝑥 ∈ 𝑦) |
| 7 | 1, 6 | eximii 1837 | 1 ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 ∀wal 1538 ∃wex 1779 |
| 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-6 1967 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-or 849 df-ex 1780 |
| This theorem is referenced by: exexneq 5439 |
| Copyright terms: Public domain | W3C validator |