MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqvisset Structured version   Visualization version   GIF version

Theorem eqvisset 3500
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.)
Assertion
Ref Expression
eqvisset (𝑥 = 𝐴𝐴 ∈ V)

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3484 . 2 𝑥 ∈ V
2 eleq1 2829 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 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