Description: Alternate proof of exel , avoiding ax-pr but requiring ax-5 , ax-9 , and ax-pow . This is similar to how elALT2 uses ax-pow instead of ax-pr compared to el . (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sn-exelALT | ⊢ ∃ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-pow | ⊢ ∃ 𝑦 ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 ) | |
| 2 | ax6ev | ⊢ ∃ 𝑥 𝑥 = 𝑧 | |
| 3 | ax9v1 | ⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) ) | |
| 4 | 3 | alrimiv | ⊢ ( 𝑥 = 𝑧 → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) ) |
| 5 | 2 4 | eximii | ⊢ ∃ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) |
| 6 | exim | ⊢ ( ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 ) → ( ∃ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → ∃ 𝑥 𝑥 ∈ 𝑦 ) ) | |
| 7 | 5 6 | mpi | ⊢ ( ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 ) → ∃ 𝑥 𝑥 ∈ 𝑦 ) |
| 8 | 1 7 | eximii | ⊢ ∃ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑦 |