Theorem eqvisset 3456

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438

This theorem is referenced by:  ceqex  3607  moeq3  3672  mo2icl  3674  eusvnfb  5332  oprabv  7409  elxp5  7856  xpsnen  8978  fival  9302  dffi2  9313  tz9.12lem1  9683  m1detdiag  22482  dvfsumlem1  25930  dchrisumlema  27397  dchrisumlem2  27399  fnimage  35903  bj-csbsnlem  36877  copsex2b  37114  pr2cv  43521  disjf1o  45169  mptssid  45219  fourierdlem49  46136