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

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

Proof of Theorem eqvisset
StepHypRef Expression
1 vex 3503 . 2 𝑥 ∈ V
2 eleq1 2905 . 2 (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
31, 2mpbii 234 1 (𝑥 = 𝐴𝐴 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1530   ∈ wcel 2107  Vcvv 3500 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-v 3502 This theorem is referenced by:  ceqex  3649  moeq3  3707  mo2icl  3709  eusvnfb  5290  oprabv  7208  elxp5  7621  xpsnen  8595  fival  8870  dffi2  8881  tz9.12lem1  9210  m1detdiag  21141  dvfsumlem1  24557  dchrisumlema  25997  dchrisumlem2  25999  fnimage  33293  bj-csbsnlem  34123  copsex2b  34330  pr2cv  39791  disjf1o  41336  mptssid  41395  fourierdlem49  42325
 Copyright terms: Public domain W3C validator