Description: A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset and issetri . (Contributed by BJ, 27-Apr-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eqvisset | |- ( x = A -> A e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | eleq1 | |- ( x = A -> ( x e. _V <-> A e. _V ) ) |
|
| 3 | 1 2 | mpbii | |- ( x = A -> A e. _V ) |