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	⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑥 𝑥 = 𝐴 )