This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issetlem

Description: Lemma for elisset and isset . (Contributed by NM, 26-May-1993) Extract from the proof of isset . (Revised by WL, 2-Feb-2025)

Ref Expression
Hypothesis issetlem.1 ⊢ 𝑥 ∈ 𝑉
Assertion issetlem ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑥 𝑥 = 𝐴 )

Proof

Step Hyp Ref Expression
1 issetlem.1 ⊢ 𝑥 ∈ 𝑉
2 dfclel ⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝑉 ) )
3 1 biantru ⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝑉 ) )
4 3 exbii ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝑉 ) )
5 2 4 bitr4i ⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑥 𝑥 = 𝐴 )