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 3504 and issetri 3508. (Contributed by BJ, 27-Apr-2019.) |
Ref | Expression |
---|---|
eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3495 | . 2 ⊢ 𝑥 ∈ V | |
2 | eleq1 2897 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
3 | 1, 2 | mpbii 234 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 Vcvv 3492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 |
This theorem is referenced by: ceqex 3642 moeq3 3700 mo2icl 3702 eusvnfb 5284 oprabv 7203 elxp5 7617 xpsnen 8589 fival 8864 dffi2 8875 tz9.12lem1 9204 m1detdiag 21134 dvfsumlem1 24550 dchrisumlema 25991 dchrisumlem2 25993 fnimage 33287 bj-csbsnlem 34117 copsex2b 34324 pr2cv 39785 disjf1o 41328 mptssid 41387 fourierdlem49 42317 |
Copyright terms: Public domain | W3C validator |