Theorem eqvisset 3483

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3467	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2857	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 236	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  ceqex  3620  moeq3  3684  mo2icl  3686  eusvnfb  5365  oprabv  7471  elxp5  7919  xpsnen  9048  fival  9371  dffi2  9382  tz9.12lem1  9758  m1detdiag  22722  dvfsumlem1  26153  dchrisumlema  27617  dchrisumlem2  27619  oldfib  28535  fnimage  36317  bj-csbsnlem  37426  copsex2b  37671  pr2cv  44165  disjf1o  45800  mptssid  45847  fourierdlem49  46760