Metamath Proof Explorer


Theorem issetft

Description: Closed theorem form of isset that does not require x and A to be distinct. Extracted from the proof of vtoclgft . (Contributed by Wolf Lammen, 9-Apr-2025)

Ref Expression
Assertion issetft _ x A A V x x = A

Proof

Step Hyp Ref Expression
1 isset A V y y = A
2 cbvexeqsetf _ x A x x = A y y = A
3 1 2 bitr4id _ x A A V x x = A