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 1570   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  ceqex  3606  moeq3  3670  mo2icl  3672  eusvnfb  5358  oprabv  7473  elxp5  7920  xpsnen  9059  fival  9382  dffi2  9393  tz9.12lem1  9769  m1detdiag  22819  dvfsumlem1  26253  dchrisumlema  27724  dchrisumlem2  27726  oldfib  28642  fnimage  36506  bj-csbsnlem  37646  copsex2b  37892  pr2cv  44388  disjf1o  46023  mptssid  46070  fourierdlem49  46983