![]() |
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 disjoint variable condition, contrary to isset 3488 and issetri 3491. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3479 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2822 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 232 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 Vcvv 3475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 |
This theorem is referenced by: ceqex 3640 moeq3 3708 mo2icl 3710 eusvnfb 5391 oprabv 7466 elxp5 7911 xpsnen 9052 fival 9404 dffi2 9415 tz9.12lem1 9779 m1detdiag 22091 dvfsumlem1 25535 dchrisumlema 26981 dchrisumlem2 26983 fnimage 34890 bj-csbsnlem 35772 copsex2b 36010 pr2cv 42285 disjf1o 43875 mptssid 43930 fourierdlem49 44858 |
Copyright terms: Public domain | W3C validator |