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

Theorem eqvisset 3114
Description: A class equal to a variable is a set. Note the absence of dv condition, contrary to isset 3110 and issetri 3113. (Contributed by BJ, 27-Apr-2019.)
Assertion
Ref Expression
eqvisset  |-  ( x  =  A  ->  A  e.  _V )

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3109 . 2  |-  x  e. 
_V
2 eleq1 2532 . 2  |-  ( x  =  A  ->  (
x  e.  _V  <->  A  e.  _V ) )
31, 2mpbii 211 1  |-  ( x  =  A  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762   _Vcvv 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-v 3108
This theorem is referenced by:  ceqex  3227  moeq3  3273  mo2icl  3275  eusvnfb  4636  oprabv  6320  elxp5  6719  xpsnen  7591  fival  7861  dffi2  7872  tz9.12lem1  8194  m1detdiag  18859  dchrisumlema  23394  fnimage  29142  bj-csbsnlem  33426
  Copyright terms: Public domain W3C validator