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

Theorem ididg 4281
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 2092 . 2 |- A = A
2 ideqg 4279 . 2 |- (A e. V -> (A _I A <-> A = A))
31, 2mpbiri 270 1 |- (A e. V -> A _I A)
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 1592   e. wcel 1594   class class class wbr 3509   _I cid 3761
This theorem is referenced by:  opelxpex2 4282  issetid 4283  fvi 4977  dfpo2 14016  eltids 14853  deref 15118
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609  ax-nul 3619  ax-pr 3679
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-v 2501  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-sn 3237  df-pr 3238  df-op 3241  df-br 3510  df-opab 3568  df-id 3765  df-xp 4151  df-rel 4152
Copyright terms: Public domain