Theorem eqvisset 3211

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

Assertion

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

Proof of Theorem eqvisset

Step	Hyp	Ref	Expression
1		vex 3203	. 2 ⊢ 𝑥 ∈ V
2		eleq1 2689	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 223	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  ceqex  3333  moeq3  3383  mo2icl  3385  eusvnfb  4862  oprabv  6703  elxp5  7111  xpsnen  8044  fival  8318  dffi2  8329  tz9.12lem1  8650  m1detdiag  20403  dvfsumlem1  23789  dchrisumlema  25177  dchrisumlem2  25179  fnimage  32036  bj-csbsnlem  32898  disjf1o  39378  mptssid  39450  fourierdlem49  40372