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

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

Proof of Theorem ididg
StepHypRef Expression
1 eqid 2075 . 2 |- A = A
2 ideqg 4262 . 2 |- (A e. V -> (A _I A <-> A = A))
31, 2mpbiri 264 1 |- (A e. V -> A _I A)
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 1573   e. wcel 1575   class class class wbr 3492   _I cid 3744
This theorem is referenced by:  opelxpex2 4265  issetid 4266  fvi 4960  dfpo2 14105  eltids 15075  deref 15340
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-14 1582  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057  ax-sep 3592  ax-nul 3602  ax-pr 3662
This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-ex 1502  df-sb 1748  df-eu 1975  df-mo 1976  df-clab 2063  df-cleq 2068  df-clel 2071  df-ne 2203  df-v 2484  df-dif 2787  df-un 2789  df-in 2791  df-ss 2793  df-nul 3049  df-sn 3220  df-pr 3221  df-op 3224  df-br 3493  df-opab 3551  df-id 3748  df-xp 4134  df-rel 4135
Copyright terms: Public domain