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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3064 . 2  |-  x  e. 
_V
2 eleq1 2476 . 2  |-  ( x  =  A  ->  (
x  e.  _V  <->  A  e.  _V ) )
31, 2mpbii 213 1  |-  ( x  =  A  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    e. wcel 1844   _Vcvv 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-12 1880  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-v 3063
This theorem is referenced by:  ceqex  3182  moeq3  3228  mo2icl  3230  eusvnfb  4592  oprabv  6328  elxp5  6731  xpsnen  7641  fival  7908  dffi2  7919  tz9.12lem1  8239  m1detdiag  19393  dvfsumlem1  22721  dchrisumlema  24056  dchrisumlem2  24058  fnimage  30280  bj-csbsnlem  31047  fourierdlem49  37319
  Copyright terms: Public domain W3C validator