Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqvisset | Structured version Visualization version GIF version |
Description: A class equal to a variable is a set. Note the absence of dv condition, contrary to isset 3180 and issetri 3183. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3176 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2676 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 222 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 |
This theorem is referenced by: ceqex 3303 moeq3 3350 mo2icl 3352 eusvnfb 4788 oprabv 6601 elxp5 7004 xpsnen 7929 fival 8201 dffi2 8212 tz9.12lem1 8533 m1detdiag 20222 dvfsumlem1 23593 dchrisumlema 24977 dchrisumlem2 24979 fnimage 31206 bj-csbsnlem 32090 disjf1o 38373 fourierdlem49 39048 |
Copyright terms: Public domain | W3C validator |