Theorem ideq 5616

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

Syntax hints:   ↔ wb 207   = wceq 1525   ∈ wcel 2083  Vcvv 3440   class class class wbr 4968   I cid 5354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457

This theorem is referenced by:  dmi  5684  resieq  5752  iss  5791  elidinxp  5799  restidsing  5807  imai  5825  intasym  5858  asymref  5859  intirr  5861  poirr2  5867  cnvi  5883  xpdifid  5908  coi1  5997  dffv2  6630  isof1oidb  6947  idssen  8409  dflt2  12395  relexpindlem  14260  opsrtoslem2  19956  hausdiag  21941  hauseqlcld  21942  metustid  22851  ltgov  26069  ex-id  27901  dfso2  32600  dfpo2  32601  idsset  32962  dfon3  32964  elfix  32975  dffix2  32977  sscoid  32985  dffun10  32986  elfuns  32987  brsingle  32989  brapply  33010  brsuccf  33013  dfrdg4  33023  iss2  35154  undmrnresiss  39470  dffrege99  39814  ipo0  40341  ifr0  40342  fourierdlem42  41998