Theorem eqvisset 3475

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  ceqex  3611  moeq3  3675  mo2icl  3677  eusvnfb  5364  oprabv  7470  elxp5  7916  xpsnen  9045  fival  9368  dffi2  9379  tz9.12lem1  9755  m1detdiag  22754  dvfsumlem1  26185  dchrisumlema  27652  dchrisumlem2  27654  oldfib  28570  fnimage  36419  bj-csbsnlem  37538  copsex2b  37784  pr2cv  44274  disjf1o  45909  mptssid  45956  fourierdlem49  46869