![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df2o3 | Structured version Visualization version Unicode version |
Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Ref | Expression |
---|---|
df2o3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 7201 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | df-suc 5436 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df1o2 7212 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | uneq1i 3575 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-pr 3962 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | eqtr4i 2496 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 6 | 3eqtri 2497 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-dif 3393 df-un 3395 df-nul 3723 df-pr 3962 df-suc 5436 df-1o 7200 df-2o 7201 |
This theorem is referenced by: df2o2 7214 2oconcl 7223 map2xp 7760 1sdom 7793 cantnflem2 8213 xp2cda 8628 sdom2en01 8750 sadcf 14506 xpscfn 15543 xpscfv 15546 xpsfrnel 15547 xpsfeq 15548 xpsfrnel2 15549 xpsle 15565 setcepi 16061 efgi0 17448 efgi1 17449 vrgpf 17496 vrgpinv 17497 frgpuptinv 17499 frgpup2 17504 frgpup3lem 17505 frgpnabllem1 17587 dmdprdpr 17760 dprdpr 17761 xpstopnlem1 20901 xpstopnlem2 20903 xpsxmetlem 21472 xpsdsval 21474 xpsmet 21475 onint1 31180 pw2f1ocnv 35963 wepwsolem 35971 |
Copyright terms: Public domain | W3C validator |