Theorem eqvisset 3500

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  ceqex  3652  moeq3  3718  mo2icl  3720  eusvnfb  5393  oprabv  7493  elxp5  7945  xpsnen  9095  fival  9452  dffi2  9463  tz9.12lem1  9827  m1detdiag  22603  dvfsumlem1  26066  dchrisumlema  27532  dchrisumlem2  27534  fnimage  35930  bj-csbsnlem  36904  copsex2b  37141  pr2cv  43561  disjf1o  45196  mptssid  45247  fourierdlem49  46170