Theorem ideq 5829

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102   I cid 5544

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657

This theorem is used by:  cnvi  5862  dmi  5902  resieq  5980  iss  6026  elidinxp  6035  restidsing  6044  imai  6071  intasym  6108  asymref  6109  intirr  6111  poirr2  6117  xpdifid  6158  coi1  6264  dfpo2  6299  dffun2  6548  dffv2  6980  isof1oidb  7332  idssen  9027  dflt2  13280  relexpindlem  15221  ex-chn1  18816  opsrtoslem2  22370  hausdiag  23969  hauseqlcld  23970  metustid  24878  ltgov  29065  ex-id  31040  dfso2  36612  idsset  36744  dfon3  36746  elfix  36757  dffix2  36759  sscoid  36767  dffun10  36768  elfuns  36769  brsingle  36771  brapply  36792  lemsuccf  36795  dfrdg4  36807  coi1in  38053  bj-imdiridlem  38199  iss2  39369  undmrnresiss  44697  dffrege99  45055  ipo0  45525  ifr0  45526  fourierdlem42  47252