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

Theorem ideq 5181
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 5180 . 2 (𝐵 ∈ V → (𝐴 I 𝐵𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 I 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976  Vcvv 3169   class class class wbr 4574   I cid 4935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-id 4940  df-xp 5031  df-rel 5032
This theorem is referenced by:  dmi  5245  resieq  5311  iss  5351  restidsing  5361  restidsingOLD  5362  imai  5381  issref  5412  intasym  5414  asymref  5415  intirr  5417  poirr2  5423  cnvi  5439  xpdifid  5464  coi1  5551  dffv2  6163  isof1oidb  6449  resiexg  6968  idssen  7860  dflt2  11813  relexpindlem  13594  opsrtoslem2  19249  hausdiag  21197  hauseqlcld  21198  metustid  22107  ltgov  25207  ex-id  26446  dfso2  30700  dfpo2  30701  idsset  30970  dfon3  30972  elfix  30983  dffix2  30985  sscoid  30993  dffun10  30994  elfuns  30995  brsingle  30997  brapply  31018  brsuccf  31021  dfrdg4  31031  undmrnresiss  36729  dffrege99  37076  ipo0  37474  ifr0  37475  fourierdlem42  38843
  Copyright terms: Public domain W3C validator