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

Theorem iss 5158
 Description: A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
iss

Proof of Theorem iss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3412 . . . . . . 7
2 vex 3034 . . . . . . . . 9
3 vex 3034 . . . . . . . . 9
42, 3opeldm 5044 . . . . . . . 8
54a1i 11 . . . . . . 7
61, 5jcad 542 . . . . . 6
7 df-br 4396 . . . . . . . . 9
83ideq 4992 . . . . . . . . 9
97, 8bitr3i 259 . . . . . . . 8
102eldm2 5038 . . . . . . . . . 10
11 opeq2 4159 . . . . . . . . . . . . . . 15
1211eleq1d 2533 . . . . . . . . . . . . . 14
1312biimprcd 233 . . . . . . . . . . . . 13
149, 13syl5bi 225 . . . . . . . . . . . 12
151, 14sylcom 29 . . . . . . . . . . 11
1615exlimdv 1787 . . . . . . . . . 10
1710, 16syl5bi 225 . . . . . . . . 9
1812imbi2d 323 . . . . . . . . 9
1917, 18syl5ibcom 228 . . . . . . . 8
209, 19syl5bi 225 . . . . . . 7
2120impd 438 . . . . . 6
226, 21impbid 195 . . . . 5
233opelres 5116 . . . . 5
2422, 23syl6bbr 271 . . . 4
2524alrimivv 1782 . . 3
26 reli 4967 . . . . 5
27 relss 4927 . . . . 5
2826, 27mpi 20 . . . 4
29 relres 5138 . . . 4
30 eqrel 4929 . . . 4
3128, 29, 30sylancl 675 . . 3
3225, 31mpbird 240 . 2
33 resss 5134 . . 3
34 sseq1 3439 . . 3
3533, 34mpbiri 241 . 2
3632, 35impbii 192 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376  wal 1450   wceq 1452  wex 1671   wcel 1904   wss 3390  cop 3965   class class class wbr 4395   cid 4749   cdm 4839   cres 4841   wrel 4844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-dm 4849  df-res 4851 This theorem is referenced by:  funcocnv2  5852  trust  21322
 Copyright terms: Public domain W3C validator