Theorem eqvisset 3492

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  ceqex  3640  moeq3  3708  mo2icl  3710  eusvnfb  5391  oprabv  7466  elxp5  7911  xpsnen  9052  fival  9404  dffi2  9415  tz9.12lem1  9779  m1detdiag  22091  dvfsumlem1  25535  dchrisumlema  26981  dchrisumlem2  26983  fnimage  34890  bj-csbsnlem  35772  copsex2b  36010  pr2cv  42285  disjf1o  43875  mptssid  43930  fourierdlem49  44858