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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3436 . 2 𝑥 ∈ V
2 eleq1 2826 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 232 1 (𝑥 = 𝐴𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2106  Vcvv 3432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434
This theorem is referenced by:  ceqex  3582  moeq3  3647  mo2icl  3649  eusvnfb  5316  oprabv  7335  elxp5  7770  xpsnen  8842  fival  9171  dffi2  9182  tz9.12lem1  9545  m1detdiag  21746  dvfsumlem1  25190  dchrisumlema  26636  dchrisumlem2  26638  fnimage  34231  bj-csbsnlem  35088  copsex2b  35311  pr2cv  41155  disjf1o  42729  mptssid  42785  fourierdlem49  43696
  Copyright terms: Public domain W3C validator