Theorem eqvisset 3508

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  ceqex  3665  moeq3  3734  mo2icl  3736  eusvnfb  5411  oprabv  7510  elxp5  7963  xpsnen  9121  fival  9481  dffi2  9492  tz9.12lem1  9856  m1detdiag  22624  dvfsumlem1  26086  dchrisumlema  27550  dchrisumlem2  27552  fnimage  35893  bj-csbsnlem  36869  copsex2b  37106  pr2cv  43510  disjf1o  45098  mptssid  45149  fourierdlem49  46076