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

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

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