Theorem eqvisset 3477

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

Assertion

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

Proof of Theorem eqvisset

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  ceqex  3613  moeq3  3677  mo2icl  3679  eusvnfb  5366  oprabv  7479  elxp5  7926  xpsnen  9056  fival  9379  dffi2  9390  tz9.12lem1  9766  m1detdiag  22804  dvfsumlem1  26236  dchrisumlema  27703  dchrisumlem2  27705  oldfib  28621  fnimage  36456  bj-csbsnlem  37595  copsex2b  37841  pr2cv  44332  disjf1o  45967  mptssid  46014  fourierdlem49  46927