Theorem eqvisset 3450

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

Assertion

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

Proof of Theorem eqvisset

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

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

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 3432

This theorem is referenced by:  ceqex  3595  moeq3  3659  mo2icl  3661  eusvnfb  5330  oprabv  7420  elxp5  7867  xpsnen  8992  fival  9318  dffi2  9329  tz9.12lem1  9702  m1detdiag  22572  dvfsumlem1  26003  dchrisumlema  27465  dchrisumlem2  27467  oldfib  28383  fnimage  36125  bj-csbsnlem  37226  copsex2b  37470  pr2cv  43993  disjf1o  45639  mptssid  45688  fourierdlem49  46601