![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fveq1i | Unicode version |
Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.) |
Ref | Expression |
---|---|
fveq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fveq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | fveq1 5428 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-rex 2423 df-uni 3745 df-br 3938 df-iota 5096 df-fv 5139 |
This theorem is referenced by: fveq12i 5435 fvun2 5496 fvopab3ig 5503 fvsnun1 5625 fvsnun2 5626 fvpr1 5632 fvpr2 5633 fvpr1g 5634 fvpr2g 5635 fvtp1g 5636 fvtp2g 5637 fvtp3g 5638 fvtp2 5640 fvtp3 5641 ov 5898 ovigg 5899 ovg 5917 tfr2a 6226 tfrex 6273 frec0g 6302 freccllem 6307 frecsuclem 6311 caseinl 6984 caseinr 6985 ctssdccl 7004 addpiord 7148 mulpiord 7149 fseq1p1m1 9905 frec2uz0d 10203 frec2uzzd 10204 frec2uzsucd 10205 frecuzrdgrrn 10212 frec2uzrdg 10213 frecuzrdg0 10217 frecuzrdgsuc 10218 frecuzrdgg 10220 frecuzrdg0t 10226 frecuzrdgsuctlem 10227 0tonninf 10243 1tonninf 10244 inftonninf 10245 seq3val 10262 seqvalcd 10263 hashinfom 10556 hashennn 10558 hashfz1 10561 shftidt 10637 resqrexlemf1 10812 resqrexlemfp1 10813 cbvsum 11161 fisumss 11193 fsumadd 11207 isumclim3 11224 cbvprod 11359 ialgr0 11761 algrp1 11763 ennnfonelem0 11954 ennnfonelemp1 11955 ennnfonelemom 11957 ctinfomlemom 11976 ndxarg 12021 strslfv2d 12040 upxp 12480 cnmetdval 12737 remetdval 12747 reeflog 12992 |
Copyright terms: Public domain | W3C validator |