Theorem eqvisset 3479

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3463	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2822	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 233	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  ceqex  3631  moeq3  3695  mo2icl  3697  eusvnfb  5363  oprabv  7467  elxp5  7919  xpsnen  9069  fival  9424  dffi2  9435  tz9.12lem1  9801  m1detdiag  22535  dvfsumlem1  25984  dchrisumlema  27451  dchrisumlem2  27453  fnimage  35947  bj-csbsnlem  36921  copsex2b  37158  pr2cv  43572  disjf1o  45215  mptssid  45265  fourierdlem49  46184