Description: A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | iss2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | |
|
2 | vex | |
|
3 | vex | |
|
4 | 2 3 | opeldm | |
5 | 1 4 | jca2 | |
6 | 2 3 | opelrn | |
7 | 1 6 | jca2 | |
8 | 5 7 | jcad | |
9 | anandi | |
|
10 | 8 9 | imbitrrdi | |
11 | df-br | |
|
12 | 3 | ideq | |
13 | 11 12 | bitr3i | |
14 | 2 | eldm2 | |
15 | opeq2 | |
|
16 | 15 | eleq1d | |
17 | 16 | biimprcd | |
18 | 13 17 | biimtrid | |
19 | 1 18 | sylcom | |
20 | 19 | exlimdv | |
21 | 14 20 | biimtrid | |
22 | 16 | imbi2d | |
23 | 21 22 | syl5ibcom | |
24 | 23 | imp | |
25 | 24 | adantrd | |
26 | 25 | ex | |
27 | 13 26 | biimtrid | |
28 | 27 | impd | |
29 | 10 28 | impbid | |
30 | opelinxp | |
|
31 | 30 | biancomi | |
32 | 29 31 | bitr4di | |
33 | 32 | alrimivv | |
34 | reli | |
|
35 | relss | |
|
36 | 34 35 | mpi | |
37 | relinxp | |
|
38 | eqrel | |
|
39 | 36 37 38 | sylancl | |
40 | 33 39 | mpbird | |
41 | inss1 | |
|
42 | sseq1 | |
|
43 | 41 42 | mpbiri | |
44 | 40 43 | impbii | |