Theorem ideq 5799

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3438   class class class wbr 5095   I cid 5517

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630

This theorem is referenced by:  dmi  5868  resieq  5945  iss  5990  elidinxp  5999  restidsing  6008  imai  6029  intasym  6068  asymref  6069  intirr  6071  poirr2  6077  cnvi  6094  xpdifid  6121  coi1  6215  dfpo2  6248  dffun2  6496  dffv2  6922  isof1oidb  7265  idssen  8929  dflt2  13068  relexpindlem  14988  opsrtoslem2  21979  hausdiag  23548  hauseqlcld  23549  metustid  24458  ltgov  28560  ex-id  30396  dfso2  35727  idsset  35863  dfon3  35865  elfix  35876  dffix2  35878  sscoid  35886  dffun10  35887  elfuns  35888  brsingle  35890  brapply  35911  brsuccf  35914  dfrdg4  35924  bj-imdiridlem  37158  iss2  38311  undmrnresiss  43577  dffrege99  43935  ipo0  44422  ifr0  44423  fourierdlem42  46131