Theorem eqvisset 3458

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  ceqex  3593  moeq3  3651  mo2icl  3653  eusvnfb  5259  oprabv  7193  elxp5  7610  xpsnen  8584  fival  8860  dffi2  8871  tz9.12lem1  9200  m1detdiag  21202  dvfsumlem1  24629  dchrisumlema  26072  dchrisumlem2  26074  fnimage  33503  bj-csbsnlem  34344  copsex2b  34555  pr2cv  40247  disjf1o  41818  mptssid  41877  fourierdlem49  42797