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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3401 . 2 𝑥 ∈ V
2 eleq1 2820 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 236 1 (𝑥 = 𝐴𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2113  Vcvv 3397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399
This theorem is referenced by:  ceqex  3546  moeq3  3609  mo2icl  3611  eusvnfb  5257  oprabv  7222  elxp5  7647  xpsnen  8643  fival  8942  dffi2  8953  tz9.12lem1  9282  m1detdiag  21341  dvfsumlem1  24770  dchrisumlema  26216  dchrisumlem2  26218  fnimage  33861  bj-csbsnlem  34709  copsex2b  34921  pr2cv  40684  disjf1o  42251  mptssid  42306  fourierdlem49  43222
  Copyright terms: Public domain W3C validator