Theorem eqvisset 3470

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3454	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2848	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 236	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  ceqex  3605  moeq3  3669  mo2icl  3671  eusvnfb  5355  oprabv  7484  elxp5  7939  xpsnen  9087  fival  9411  dffi2  9422  tz9.12lem1  9801  m1detdiag  22921  dvfsumlem1  26355  dchrisumlema  27824  dchrisumlem2  27826  oldfib  28772  fnimage  36787  bj-csbsnlem  37911  copsex2b  38170  pr2cv  44658  disjf1o  46314  mptssid  46361  fourierdlem49  47273