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 3410 and issetri 3413. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3401 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2820 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 236 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2113 Vcvv 3397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 |
This theorem is referenced by: ceqex 3546 moeq3 3609 mo2icl 3611 eusvnfb 5257 oprabv 7222 elxp5 7647 xpsnen 8643 fival 8942 dffi2 8953 tz9.12lem1 9282 m1detdiag 21341 dvfsumlem1 24770 dchrisumlema 26216 dchrisumlem2 26218 fnimage 33861 bj-csbsnlem 34709 copsex2b 34921 pr2cv 40684 disjf1o 42251 mptssid 42306 fourierdlem49 43222 |
Copyright terms: Public domain | W3C validator |