Theorem eqvisset 3451

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3435	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2827	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 234	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  ceqex  3590  moeq3  3653  mo2icl  3655  eusvnfb  5322  oprabv  7416  elxp5  7863  xpsnen  8989  fival  9315  dffi2  9326  tz9.12lem1  9702  m1detdiag  22580  dvfsumlem1  26011  dchrisumlema  27469  dchrisumlem2  27471  oldfib  28387  fnimage  36155  bj-csbsnlem  37256  copsex2b  37500  pr2cv  43992  disjf1o  45638  mptssid  45685  fourierdlem49  46598