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 x V
Assertion issetlem A V x x = A

Proof

Step Hyp Ref Expression
1 issetlem.1 x V
2 dfclel A V x x = A x V
3 1 biantru x = A x = A x V
4 3 exbii x x = A x x = A x V
5 2 4 bitr4i A V x x = A