Theorem eqvisset 3449

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

Assertion

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

Proof of Theorem eqvisset

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  ceqex  3594  moeq3  3658  mo2icl  3660  eusvnfb  5335  oprabv  7427  elxp5  7874  xpsnen  8999  fival  9325  dffi2  9336  tz9.12lem1  9711  m1detdiag  22562  dvfsumlem1  25993  dchrisumlema  27451  dchrisumlem2  27453  oldfib  28369  fnimage  36109  bj-csbsnlem  37210  copsex2b  37454  pr2cv  43975  disjf1o  45621  mptssid  45670  fourierdlem49  46583