![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df2o3 | 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 6435 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | df-suc 4385 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df1o2 6447 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | uneq1i 3299 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-pr 3613 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | eqtr4i 2212 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 6 | 3eqtri 2213 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2175 df-cleq 2181 df-clel 2184 df-nfc 2320 df-v 2753 df-dif 3145 df-un 3147 df-nul 3437 df-pr 3613 df-suc 4385 df-1o 6434 df-2o 6435 |
This theorem is referenced by: df2o2 6449 2oconcl 6457 0lt2o 6459 1lt2o 6460 el2oss1o 6461 en2eqpr 6924 nninfisol 7148 finomni 7155 exmidomniim 7156 exmidomni 7157 ismkvnex 7170 nninfwlpoimlemginf 7191 exmidfodomrlemr 7218 exmidfodomrlemrALT 7219 xp2dju 7231 pw1nel3 7247 sucpw1nel3 7249 unct 12460 fnpr2o 12780 fnpr2ob 12781 fvprif 12784 xpsfrnel 12785 xpsfeq 12786 2o01f 15130 nninfalllem1 15141 nninfall 15142 nninfsellemqall 15148 nninfomnilem 15151 |
Copyright terms: Public domain | W3C validator |