![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ixpfn | Structured version Visualization version Unicode version |
Description: A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
Ref | Expression |
---|---|
ixpfn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 5674 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elixp2 7544 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | simp2bi 1046 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | vtoclga 3099 |
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-3an 1009 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-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-iota 5553 df-fun 5591 df-fn 5592 df-fv 5597 df-ixp 7541 |
This theorem is referenced by: ixpprc 7561 undifixp 7576 resixpfo 7578 boxcutc 7583 ixpiunwdom 8124 prdsbasfn 15447 xpsff1o 15552 sscfn1 15800 funcfn2 15852 natfn 15937 pthaus 20730 ptuncnv 20899 ptunhmeo 20900 ptcmplem2 21146 prdsbl 21584 finixpnum 31994 upixp 32120 prdstotbnd 32190 hoidmvlelem3 38537 hspdifhsp 38556 hspmbllem2 38567 |
Copyright terms: Public domain | W3C validator |