Theorem eqvisset 3462

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444

This theorem is referenced by:  ceqex  3608  moeq3  3672  mo2icl  3674  eusvnfb  5340  oprabv  7428  elxp5  7875  xpsnen  9001  fival  9327  dffi2  9338  tz9.12lem1  9711  m1detdiag  22553  dvfsumlem1  26000  dchrisumlema  27467  dchrisumlem2  27469  oldfib  28385  fnimage  36143  bj-csbsnlem  37151  copsex2b  37395  pr2cv  43904  disjf1o  45550  mptssid  45599  fourierdlem49  46513