Description: An element of a class exists. Use elissetv instead when sufficient (for instance in usages where x is a dummy variable). (Contributed by NM, 1-May-1995) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | elisset | ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elissetv | ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑧 𝑧 = 𝐴 ) | |
2 | iseqsetv-clel | ⊢ ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑥 𝑥 = 𝐴 ) | |
3 | 1 2 | sylib | ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 ) |