Metamath Proof Explorer


Theorem elissetv

Description: An element of a class exists. Version of elisset with a disjoint variable condition on V , x , avoiding df-clab . Prefer its use over elisset when sufficient (for instance in usages where x is a dummy variable). (Contributed by BJ, 14-Sep-2019)

Ref Expression
Assertion elissetv AVxx=A

Proof

Step Hyp Ref Expression
1 dfclel AVxx=AxV
2 exsimpl xx=AxVxx=A
3 1 2 sylbi AVxx=A