Theorem eqvisset 3464

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  ceqex  3615  moeq3  3680  mo2icl  3682  eusvnfb  5343  oprabv  7429  elxp5  7879  xpsnen  9002  fival  9339  dffi2  9350  tz9.12lem1  9716  m1detdiag  22460  dvfsumlem1  25908  dchrisumlema  27375  dchrisumlem2  27377  fnimage  35890  bj-csbsnlem  36864  copsex2b  37101  pr2cv  43510  disjf1o  45158  mptssid  45208  fourierdlem49  46126