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

Theorem eqvisset 3209
Description: A class equal to a variable is a set. Note the absence of dv condition, contrary to isset 3205 and issetri 3208. (Contributed by BJ, 27-Apr-2019.)
Assertion
Ref Expression
eqvisset (𝑥 = 𝐴𝐴 ∈ V)

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3201 . 2 𝑥 ∈ V
2 eleq1 2688 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 223 1 (𝑥 = 𝐴𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  wcel 1989  Vcvv 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-12 2046  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1485  df-ex 1704  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3200
This theorem is referenced by:  ceqex  3331  moeq3  3381  mo2icl  3383  eusvnfb  4860  oprabv  6700  elxp5  7108  xpsnen  8041  fival  8315  dffi2  8326  tz9.12lem1  8647  m1detdiag  20397  dvfsumlem1  23783  dchrisumlema  25171  dchrisumlem2  25173  fnimage  32020  bj-csbsnlem  32882  disjf1o  39200  mptssid  39272  fourierdlem49  40141
  Copyright terms: Public domain W3C validator