Theorem eqvisset 3458

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  ceqex  3604  moeq3  3668  mo2icl  3670  eusvnfb  5336  oprabv  7416  elxp5  7863  xpsnen  8987  fival  9313  dffi2  9324  tz9.12lem1  9697  m1detdiag  22539  dvfsumlem1  25986  dchrisumlema  27453  dchrisumlem2  27455  oldfib  28335  fnimage  36070  bj-csbsnlem  37047  copsex2b  37284  pr2cv  43731  disjf1o  45377  mptssid  45427  fourierdlem49  46341