| 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 3494 and issetri 3499. (Contributed by BJ, 27-Apr-2019.) |
| Ref | Expression |
|---|---|
| eqvisset | ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3484 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | eleq1 2829 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V)) | |
| 3 | 1, 2 | mpbii 233 | 1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 |
| This theorem is referenced by: ceqex 3652 moeq3 3718 mo2icl 3720 eusvnfb 5393 oprabv 7493 elxp5 7945 xpsnen 9095 fival 9452 dffi2 9463 tz9.12lem1 9827 m1detdiag 22603 dvfsumlem1 26066 dchrisumlema 27532 dchrisumlem2 27534 fnimage 35930 bj-csbsnlem 36904 copsex2b 37141 pr2cv 43561 disjf1o 45196 mptssid 45247 fourierdlem49 46170 |
| Copyright terms: Public domain | W3C validator |