Description: Every set is an element of some other set. See elALT for a shorter proof using more axioms, and see elALT2 for a proof that uses ax-9 and ax-pow instead of ax-pr . (Contributed by NM, 4-Jan-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) Avoid ax-9 , ax-pow . (Revised by BTernaryTau, 2-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | el | ⊢ ∃ 𝑦 𝑥 ∈ 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-pr | ⊢ ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝑦 ) | |
| 2 | pm4.25 | ⊢ ( 𝑧 = 𝑥 ↔ ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) ) | |
| 3 | 2 | imbi1i | ⊢ ( ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ( ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝑦 ) ) |
| 4 | 3 | albii | ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝑦 ) ) |
| 5 | elequ1 | ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) ) | |
| 6 | 5 | equsalvw | ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → 𝑧 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝑦 ) |
| 7 | 4 6 | bitr3i | ⊢ ( ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝑦 ) |
| 8 | 7 | exbii | ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑧 = 𝑥 ∨ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 𝑥 ∈ 𝑦 ) |
| 9 | 1 8 | mpbi | ⊢ ∃ 𝑦 𝑥 ∈ 𝑦 |