Theorem eqvisset 3474

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3458	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2850	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 235	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456

This theorem is referenced by:  ceqex  3611  moeq3  3675  mo2icl  3677  eusvnfb  5350  oprabv  7456  elxp5  7904  xpsnen  9033  fival  9358  dffi2  9369  tz9.12lem1  9745  m1detdiag  22654  dvfsumlem1  26085  dchrisumlema  27549  dchrisumlem2  27551  oldfib  28467  fnimage  36274  bj-csbsnlem  37385  copsex2b  37629  pr2cv  44121  disjf1o  45766  mptssid  45813  fourierdlem49  46726