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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3344 . 2 𝑥 ∈ V
2 eleq1 2828 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 223 1 (𝑥 = 𝐴𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2140  Vcvv 3341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-12 2197  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1635  df-ex 1854  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-v 3343
This theorem is referenced by:  ceqex  3473  moeq3  3525  mo2icl  3527  eusvnfb  5012  oprabv  6870  elxp5  7278  xpsnen  8212  fival  8486  dffi2  8497  tz9.12lem1  8826  m1detdiag  20626  dvfsumlem1  24009  dchrisumlema  25398  dchrisumlem2  25400  fnimage  32364  bj-csbsnlem  33221  disjf1o  39896  mptssid  39968  fourierdlem49  40894
  Copyright terms: Public domain W3C validator