Theorem ideq 5841

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  Vcvv 3458   class class class wbr 5112   I cid 5558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5260  ax-pr 5407

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5113  df-opab 5177  df-id 5559  df-xp 5670  df-rel 5671

This theorem is used by:  cnvi  5874  dmi  5914  resieq  5992  iss  6040  elidinxp  6049  restidsing  6058  imai  6079  intasym  6118  asymref  6119  intirr  6121  poirr2  6127  xpdifid  6168  coi1  6267  dfpo2  6301  dffun2  6550  dffv2  6980  isof1oidb  7326  idssen  8996  dflt2  13183  relexpindlem  15111  ex-chn1  18703  opsrtoslem2  22222  hausdiag  23817  hauseqlcld  23818  metustid  24726  ltgov  28881  ex-id  30800  dfso2  36259  idsset  36392  dfon3  36394  elfix  36405  dffix2  36407  sscoid  36415  dffun10  36416  elfuns  36417  brsingle  36419  brapply  36440  lemsuccf  36443  dfrdg4  36455  bj-imdiridlem  37861  iss2  39025  undmrnresiss  44362  dffrege99  44720  ipo0  45190  ifr0  45191  fourierdlem42  46895