Theorem ideq 5819

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 5818	. 2 ⊢ (𝐵 ∈ V → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110   I cid 5535

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648

This theorem is referenced by:  dmi  5888  resieq  5964  iss  6009  elidinxp  6018  restidsing  6027  imai  6048  intasym  6091  asymref  6092  intirr  6094  poirr2  6100  cnvi  6117  xpdifid  6144  coi1  6238  dfpo2  6272  dffun2  6524  dffun2OLD  6525  dffv2  6959  isof1oidb  7302  idssen  8971  dflt2  13115  relexpindlem  15036  opsrtoslem2  21970  hausdiag  23539  hauseqlcld  23540  metustid  24449  ltgov  28531  ex-id  30370  dfso2  35749  idsset  35885  dfon3  35887  elfix  35898  dffix2  35900  sscoid  35908  dffun10  35909  elfuns  35910  brsingle  35912  brapply  35933  brsuccf  35936  dfrdg4  35946  bj-imdiridlem  37180  iss2  38333  undmrnresiss  43600  dffrege99  43958  ipo0  44445  ifr0  44446  fourierdlem42  46154