Theorem ideq 5816

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3447   class class class wbr 5107   I cid 5532

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645

This theorem is referenced by:  dmi  5885  resieq  5961  iss  6006  elidinxp  6015  restidsing  6024  imai  6045  intasym  6088  asymref  6089  intirr  6091  poirr2  6097  cnvi  6114  xpdifid  6141  coi1  6235  dfpo2  6269  dffun2  6521  dffun2OLD  6522  dffv2  6956  isof1oidb  7299  idssen  8968  dflt2  13108  relexpindlem  15029  opsrtoslem2  21963  hausdiag  23532  hauseqlcld  23533  metustid  24442  ltgov  28524  ex-id  30363  dfso2  35742  idsset  35878  dfon3  35880  elfix  35891  dffix2  35893  sscoid  35901  dffun10  35902  elfuns  35903  brsingle  35905  brapply  35926  brsuccf  35929  dfrdg4  35939  bj-imdiridlem  37173  iss2  38326  undmrnresiss  43593  dffrege99  43951  ipo0  44438  ifr0  44439  fourierdlem42  46147