Theorem eqvisset 3470

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

Assertion

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

Proof of Theorem eqvisset

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  ceqex  3621  moeq3  3686  mo2icl  3688  eusvnfb  5351  oprabv  7452  elxp5  7902  xpsnen  9029  fival  9370  dffi2  9381  tz9.12lem1  9747  m1detdiag  22491  dvfsumlem1  25939  dchrisumlema  27406  dchrisumlem2  27408  fnimage  35924  bj-csbsnlem  36898  copsex2b  37135  pr2cv  43544  disjf1o  45192  mptssid  45242  fourierdlem49  46160