![]() |
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 3492 and issetri 3497. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3482 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2827 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 233 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 Vcvv 3478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 |
This theorem is referenced by: ceqex 3652 moeq3 3721 mo2icl 3723 eusvnfb 5399 oprabv 7493 elxp5 7946 xpsnen 9094 fival 9450 dffi2 9461 tz9.12lem1 9825 m1detdiag 22619 dvfsumlem1 26081 dchrisumlema 27547 dchrisumlem2 27549 fnimage 35911 bj-csbsnlem 36886 copsex2b 37123 pr2cv 43538 disjf1o 45134 mptssid 45185 fourierdlem49 46111 |
Copyright terms: Public domain | W3C validator |