HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ididg 4411
Description: A set is identical to itself. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
ididg

Proof of Theorem ididg
StepHypRef Expression
1 eqid 2090 . 2
2 ideqg 4409 . 2
31, 2mpbiri 222 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1531   wcel 1533   class class class wbr 3591   cid 3843
This theorem is referenced by:  issetid  4412  fvi  5174  dfpo2  18793  eltids  19673  deref  19921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pr 3756
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-br 3592  df-opab 3645  df-id 3848  df-xp 4263  df-rel 4264
Copyright terms: Public domain