![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reseq1i | Unicode version |
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
Ref | Expression |
---|---|
reseqi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reseq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseqi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | reseq1 4739 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-in 3019 df-res 4479 |
This theorem is referenced by: reseq12i 4743 resindm 4787 resmpt 4793 resmpt3 4794 resmptf 4795 opabresid 4798 rescnvcnv 4927 coires1 4982 fcoi1 5226 fvsnun1 5533 fvsnun2 5534 resoprab 5779 resmpt2 5781 ofmres 5945 f1stres 5968 f2ndres 5969 df1st2 6022 df2nd2 6023 dftpos2 6064 tfr2a 6124 freccllem 6205 frecfcllem 6207 frecsuclem 6209 djuf1olemr 6826 divfnzn 9205 cnmptid 12119 xmsxmet2 12265 msmet2 12266 |
Copyright terms: Public domain | W3C validator |