Theorem eqvisset 3439

Description: A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 3435 and issetri 3438. (Contributed by BJ, 27-Apr-2019.)

Assertion

Ref	Expression
eqvisset	⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3426	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2826	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 232	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  ceqex  3574  moeq3  3642  mo2icl  3644  eusvnfb  5311  oprabv  7313  elxp5  7744  xpsnen  8796  fival  9101  dffi2  9112  tz9.12lem1  9476  m1detdiag  21654  dvfsumlem1  25095  dchrisumlema  26541  dchrisumlem2  26543  fnimage  34158  bj-csbsnlem  35015  copsex2b  35238  pr2cv  41044  disjf1o  42618  mptssid  42674  fourierdlem49  43586