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

Theorem ididg 4332
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 2030 . 2
2 ideqg 4330 . 2
31, 2mpbiri 222 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1526   wcel 1528   class class class wbr 3531   cid 3782
This theorem is referenced by:  issetid 4333  fvi 5091  dfpo2 18488  eltids 19378  deref 19627
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626  ax-nul 3635  ax-pr 3695
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-sn 3214  df-pr 3215  df-op 3217  df-br 3532  df-opab 3585  df-id 3787  df-xp 4186  df-rel 4187
Copyright terms: Public domain