Theorem eqvisset 3449

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434

This theorem is referenced by:  ceqex  3582  moeq3  3647  mo2icl  3649  eusvnfb  5316  oprabv  7335  elxp5  7770  xpsnen  8842  fival  9171  dffi2  9182  tz9.12lem1  9545  m1detdiag  21746  dvfsumlem1  25190  dchrisumlema  26636  dchrisumlem2  26638  fnimage  34231  bj-csbsnlem  35088  copsex2b  35311  pr2cv  41155  disjf1o  42729  mptssid  42785  fourierdlem49  43696