Theorem eqvisset 3352

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2140  Vcvv 3341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-12 2197  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1635  df-ex 1854  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-v 3343

This theorem is referenced by:  ceqex  3473  moeq3  3525  mo2icl  3527  eusvnfb  5012  oprabv  6870  elxp5  7278  xpsnen  8212  fival  8486  dffi2  8497  tz9.12lem1  8826  m1detdiag  20626  dvfsumlem1  24009  dchrisumlema  25398  dchrisumlem2  25400  fnimage  32364  bj-csbsnlem  33221  disjf1o  39896  mptssid  39968  fourierdlem49  40894