Theorem eqvisset 3491

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  ceqex  3640  moeq3  3708  mo2icl  3710  eusvnfb  5391  oprabv  7471  elxp5  7916  xpsnen  9057  fival  9409  dffi2  9420  tz9.12lem1  9784  m1detdiag  22106  dvfsumlem1  25550  dchrisumlema  26998  dchrisumlem2  27000  fnimage  34970  bj-csbsnlem  35869  copsex2b  36107  pr2cv  42381  disjf1o  43969  mptssid  44023  fourierdlem49  44950