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

Theorem ideq 5809
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 5808 . 2 (𝐵 ∈ V → (𝐴 I 𝐵𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 I 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107  Vcvv 3444   class class class wbr 5106   I cid 5531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641
This theorem is referenced by:  dmi  5878  resieq  5949  iss  5990  elidinxp  5998  restidsing  6007  imai  6027  intasym  6070  asymref  6071  intirr  6073  poirr2  6079  cnvi  6095  xpdifid  6121  coi1  6215  dfpo2  6249  dffun2  6507  dffun2OLD  6508  dffv2  6937  isof1oidb  7270  idssen  8940  dflt2  13073  relexpindlem  14954  opsrtoslem2  21479  hausdiag  23012  hauseqlcld  23013  metustid  23926  ltgov  27581  ex-id  29420  dfso2  34384  idsset  34521  dfon3  34523  elfix  34534  dffix2  34536  sscoid  34544  dffun10  34545  elfuns  34546  brsingle  34548  brapply  34569  brsuccf  34572  dfrdg4  34582  bj-imdiridlem  35702  iss2  36851  undmrnresiss  41964  dffrege99  42322  ipo0  42817  ifr0  42818  fourierdlem42  44476
  Copyright terms: Public domain W3C validator