Theorem ideq 5837

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)

Hypothesis

Ref	Expression
ideq.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ideq	⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Proof of Theorem ideq

Step	Hyp	Ref	Expression
1		ideq.1	. 2 ⊢ 𝐵 ∈ V
2		ideqg 5836	. 2 ⊢ (𝐵 ∈ V → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3464   class class class wbr 5124   I cid 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666

This theorem is referenced by:  dmi  5906  resieq  5982  iss  6027  elidinxp  6036  restidsing  6045  imai  6066  intasym  6109  asymref  6110  intirr  6112  poirr2  6118  cnvi  6135  xpdifid  6162  coi1  6256  dfpo2  6290  dffun2  6546  dffun2OLD  6547  dffv2  6979  isof1oidb  7322  idssen  9016  dflt2  13169  relexpindlem  15087  opsrtoslem2  22019  hausdiag  23588  hauseqlcld  23589  metustid  24498  ltgov  28581  ex-id  30420  dfso2  35777  idsset  35913  dfon3  35915  elfix  35926  dffix2  35928  sscoid  35936  dffun10  35937  elfuns  35938  brsingle  35940  brapply  35961  brsuccf  35964  dfrdg4  35974  bj-imdiridlem  37208  iss2  38367  undmrnresiss  43595  dffrege99  43953  ipo0  44440  ifr0  44441  fourierdlem42  46145