Theorem eqvisset 3414

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3401	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2820	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 236	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2113  Vcvv 3397

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399

This theorem is referenced by:  ceqex  3546  moeq3  3609  mo2icl  3611  eusvnfb  5257  oprabv  7222  elxp5  7647  xpsnen  8643  fival  8942  dffi2  8953  tz9.12lem1  9282  m1detdiag  21341  dvfsumlem1  24770  dchrisumlema  26216  dchrisumlem2  26218  fnimage  33861  bj-csbsnlem  34709  copsex2b  34921  pr2cv  40684  disjf1o  42251  mptssid  42306  fourierdlem49  43222