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

Theorem ideq 5426
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 5425 . 2 (𝐵 ∈ V → (𝐴 I 𝐵𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 I 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1628  wcel 2135  Vcvv 3336   class class class wbr 4800   I cid 5169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4801  df-opab 4861  df-id 5170  df-xp 5268  df-rel 5269
This theorem is referenced by:  dmi  5491  resieq  5561  iss  5601  restidsing  5612  restidsingOLD  5613  imai  5632  issref  5663  intasym  5665  asymref  5666  intirr  5668  poirr2  5674  cnvi  5691  xpdifid  5716  coi1  5808  dffv2  6429  isof1oidb  6733  resiexg  7263  idssen  8162  dflt2  12170  relexpindlem  13998  opsrtoslem2  19683  hausdiag  21646  hauseqlcld  21647  metustid  22556  ltgov  25687  ex-id  27598  dfso2  31947  dfpo2  31948  idsset  32299  dfon3  32301  elfix  32312  dffix2  32314  sscoid  32322  dffun10  32323  elfuns  32324  brsingle  32326  brapply  32347  brsuccf  32350  dfrdg4  32360  iss2  34431  undmrnresiss  38408  dffrege99  38754  ipo0  39151  ifr0  39152  fourierdlem42  40865
  Copyright terms: Public domain W3C validator