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 2848	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
3	1, 2	mpbii 236	1 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  ceqex  3605  moeq3  3669  mo2icl  3671  eusvnfb  5354  oprabv  7480  elxp5  7935  xpsnen  9080  fival  9404  dffi2  9415  tz9.12lem1  9794  m1detdiag  22912  dvfsumlem1  26346  dchrisumlema  27815  dchrisumlem2  27817  oldfib  28763  fnimage  36691  bj-csbsnlem  37815  copsex2b  38062  pr2cv  44549  disjf1o  46206  mptssid  46253  fourierdlem49  47165