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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3479 . 2 𝑥 ∈ V
2 eleq1 2822 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 232 1 (𝑥 = 𝐴𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3475
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477
This theorem is referenced by:  ceqex  3640  moeq3  3708  mo2icl  3710  eusvnfb  5391  oprabv  7466  elxp5  7911  xpsnen  9052  fival  9404  dffi2  9415  tz9.12lem1  9779  m1detdiag  22091  dvfsumlem1  25535  dchrisumlema  26981  dchrisumlem2  26983  fnimage  34890  bj-csbsnlem  35772  copsex2b  36010  pr2cv  42285  disjf1o  43875  mptssid  43930  fourierdlem49  44858
  Copyright terms: Public domain W3C validator