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 3445 and issetri 3448. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3436 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2826 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 232 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 Vcvv 3432 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 |
This theorem is referenced by: ceqex 3582 moeq3 3647 mo2icl 3649 eusvnfb 5316 oprabv 7335 elxp5 7770 xpsnen 8842 fival 9171 dffi2 9182 tz9.12lem1 9545 m1detdiag 21746 dvfsumlem1 25190 dchrisumlema 26636 dchrisumlem2 26638 fnimage 34231 bj-csbsnlem 35088 copsex2b 35311 pr2cv 41155 disjf1o 42729 mptssid 42785 fourierdlem49 43696 |
Copyright terms: Public domain | W3C validator |