Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssrel | Structured version Visualization version Unicode version |
Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Remove dependency on ax-sep 4781, ax-nul 4789, ax-pr 4906. (Revised by KP, 25-Oct-2021.) |
Ref | Expression |
---|---|
ssrel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3597 | . . 3 | |
2 | 1 | alrimivv 1856 | . 2 |
3 | df-rel 5121 | . . . . . . 7 | |
4 | dfss2 3591 | . . . . . . 7 | |
5 | 3, 4 | sylbb 209 | . . . . . 6 |
6 | df-xp 5120 | . . . . . . . . . 10 | |
7 | df-opab 4713 | . . . . . . . . . 10 | |
8 | 6, 7 | eqtri 2644 | . . . . . . . . 9 |
9 | 8 | abeq2i 2735 | . . . . . . . 8 |
10 | simpl 473 | . . . . . . . . 9 | |
11 | 10 | 2eximi 1763 | . . . . . . . 8 |
12 | 9, 11 | sylbi 207 | . . . . . . 7 |
13 | 12 | imim2i 16 | . . . . . 6 |
14 | 5, 13 | sylg 1750 | . . . . 5 |
15 | eleq1 2689 | . . . . . . . . . . . 12 | |
16 | eleq1 2689 | . . . . . . . . . . . 12 | |
17 | 15, 16 | imbi12d 334 | . . . . . . . . . . 11 |
18 | 17 | biimprcd 240 | . . . . . . . . . 10 |
19 | 18 | 2alimi 1740 | . . . . . . . . 9 |
20 | 19.23vv 1903 | . . . . . . . . 9 | |
21 | 19, 20 | sylib 208 | . . . . . . . 8 |
22 | 21 | com23 86 | . . . . . . 7 |
23 | 22 | a2d 29 | . . . . . 6 |
24 | 23 | alimdv 1845 | . . . . 5 |
25 | 14, 24 | syl5 34 | . . . 4 |
26 | dfss2 3591 | . . . 4 | |
27 | 25, 26 | syl6ibr 242 | . . 3 |
28 | 27 | com12 32 | . 2 |
29 | 2, 28 | impbid2 216 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wal 1481 wceq 1483 wex 1704 wcel 1990 cab 2608 cvv 3200 wss 3574 cop 4183 copab 4712 cxp 5112 wrel 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-opab 4713 df-xp 5120 df-rel 5121 |
This theorem is referenced by: eqrel 5209 relssi 5211 relssdv 5212 cotrg 5507 cnvsym 5510 intasym 5511 intirr 5514 codir 5516 qfto 5517 dfso2 31644 dfpo2 31645 dffun10 32021 imagesset 32060 ssrel3 34067 undmrnresiss 37910 cnvssco 37912 |
Copyright terms: Public domain | W3C validator |