Theorem eqvisset 3491

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3478	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2821	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 232	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  ceqex  3639  moeq3  3707  mo2icl  3709  eusvnfb  5390  oprabv  7465  elxp5  7910  xpsnen  9051  fival  9403  dffi2  9414  tz9.12lem1  9778  m1detdiag  22090  dvfsumlem1  25534  dchrisumlema  26980  dchrisumlem2  26982  fnimage  34889  bj-csbsnlem  35771  copsex2b  36009  pr2cv  42284  disjf1o  43874  mptssid  43929  fourierdlem49  44857