MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ideq Structured version   Visualization version   GIF version

Theorem ideq 5445
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
StepHypRef Expression
1 ideq.1 . 2 𝐵 ∈ V
2 ideqg 5444 . 2 (𝐵 ∈ V → (𝐴 I 𝐵𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 I 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  wcel 2155  Vcvv 3350   class class class wbr 4811   I cid 5186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-id 5187  df-xp 5285  df-rel 5286
This theorem is referenced by:  dmi  5510  resieq  5585  iss  5626  elidinxp  5634  elridOLD  5637  restidsing  5644  imai  5662  idrefOLD  5694  intasym  5696  asymref  5697  intirr  5699  poirr2  5705  cnvi  5722  xpdifid  5747  coi1  5839  dffv2  6462  isof1oidb  6768  idssen  8207  dflt2  12184  relexpindlem  14091  opsrtoslem2  19761  hausdiag  21731  hauseqlcld  21732  metustid  22641  ltgov  25786  ex-id  27753  dfso2  32092  dfpo2  32093  idsset  32444  dfon3  32446  elfix  32457  dffix2  32459  sscoid  32467  dffun10  32468  elfuns  32469  brsingle  32471  brapply  32492  brsuccf  32495  dfrdg4  32505  iss2  34544  undmrnresiss  38588  dffrege99  38933  ipo0  39328  ifr0  39329  fourierdlem42  41006
  Copyright terms: Public domain W3C validator