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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfclel | |
|
2 | exsimpl | |
|
3 | 1 2 | sylbi | |