Theorem eqvisset 3467

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3451	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2816	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 233	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  ceqex  3618  moeq3  3683  mo2icl  3685  eusvnfb  5348  oprabv  7449  elxp5  7899  xpsnen  9025  fival  9363  dffi2  9374  tz9.12lem1  9740  m1detdiag  22484  dvfsumlem1  25932  dchrisumlema  27399  dchrisumlem2  27401  fnimage  35917  bj-csbsnlem  36891  copsex2b  37128  pr2cv  43537  disjf1o  45185  mptssid  45235  fourierdlem49  46153