Theorem eqvisset 3471

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

Assertion

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

Proof of Theorem eqvisset

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  ceqex  3606  moeq3  3670  mo2icl  3672  eusvnfb  5355  oprabv  7478  elxp5  7933  xpsnen  9073  fival  9397  dffi2  9408  tz9.12lem1  9787  m1detdiag  22905  dvfsumlem1  26339  dchrisumlema  27808  dchrisumlem2  27810  oldfib  28756  fnimage  36671  bj-csbsnlem  37795  copsex2b  38041  pr2cv  44533  disjf1o  46175  mptssid  46222  fourierdlem49  47134