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

Theorem ideq 5691
 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 5690 . 2 (𝐵 ∈ V → (𝐴 I 𝐵𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 I 𝐵𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2112  Vcvv 3444   class class class wbr 5033   I cid 5427 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530 This theorem is referenced by:  dmi  5759  resieq  5833  iss  5874  elidinxp  5882  restidsing  5893  imai  5913  intasym  5946  asymref  5947  intirr  5949  poirr2  5955  cnvi  5971  xpdifid  5996  coi1  6086  dffv2  6737  isof1oidb  7060  idssen  8541  dflt2  12533  relexpindlem  14417  opsrtoslem2  20727  hausdiag  22253  hauseqlcld  22254  metustid  23164  ltgov  26394  ex-id  28222  dfso2  33098  dfpo2  33099  idsset  33459  dfon3  33461  elfix  33472  dffix2  33474  sscoid  33482  dffun10  33483  elfuns  33484  brsingle  33486  brapply  33507  brsuccf  33510  dfrdg4  33520  bj-imdiridlem  34595  iss2  35754  undmrnresiss  40291  dffrege99  40650  ipo0  41140  ifr0  41141  fourierdlem42  42778
 Copyright terms: Public domain W3C validator