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

Theorem iss 5192
 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 3344 . . . . . . 7
2 vex 2961 . . . . . . . . 9
3 vex 2961 . . . . . . . . 9
42, 3opeldm 5076 . . . . . . . 8
54a1i 11 . . . . . . 7
61, 5jcad 521 . . . . . 6
7 df-br 4216 . . . . . . . . 9
83ideq 5028 . . . . . . . . 9
97, 8bitr3i 244 . . . . . . . 8
102eldm2 5071 . . . . . . . . . 10
11 opeq2 3987 . . . . . . . . . . . . . . 15
1211eleq1d 2504 . . . . . . . . . . . . . 14
1312biimprcd 218 . . . . . . . . . . . . 13
149, 13syl5bi 210 . . . . . . . . . . . 12
151, 14sylcom 28 . . . . . . . . . . 11
1615exlimdv 1647 . . . . . . . . . 10
1710, 16syl5bi 210 . . . . . . . . 9
1812imbi2d 309 . . . . . . . . 9
1917, 18syl5ibcom 213 . . . . . . . 8
209, 19syl5bi 210 . . . . . . 7
2120imp3a 422 . . . . . 6
226, 21impbid 185 . . . . 5
233opelres 5154 . . . . 5
2422, 23syl6bbr 256 . . . 4
2524alrimivv 1643 . . 3
26 reli 5005 . . . . 5
27 relss 4966 . . . . 5
2826, 27mpi 17 . . . 4
29 relres 5177 . . . 4
30 eqrel 4968 . . . 4
3128, 29, 30sylancl 645 . . 3
3225, 31mpbird 225 . 2
33 resss 5173 . . 3
34 sseq1 3371 . . 3
3533, 34mpbiri 226 . 2
3632, 35impbii 182 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wal 1550  wex 1551   wceq 1653   wcel 1726   wss 3322  cop 3819   class class class wbr 4215   cid 4496   cdm 4881   cres 4883   wrel 4886 This theorem is referenced by:  funcocnv2  5703  trust  18264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-id 4501  df-xp 4887  df-rel 4888  df-dm 4891  df-res 4893
 Copyright terms: Public domain W3C validator