![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ixpfn | Structured 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 5608 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elixp2 7378 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | simp2bi 1004 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | vtoclga 3142 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ral 2804 df-rex 2805 df-rab 2808 df-v 3080 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-br 4402 df-opab 4460 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-iota 5490 df-fun 5529 df-fn 5530 df-fv 5535 df-ixp 7375 |
This theorem is referenced by: ixpprc 7395 undifixp 7410 resixpfo 7412 boxcutc 7417 ixpiunwdom 7918 prdsbasfn 14529 xpsff1o 14626 sscfn1 14850 funcfn2 14899 natfn 14984 dprdvalOLD 16610 pthaus 19344 ptuncnv 19513 ptunhmeo 19514 ptcmplem2 19758 prdsbl 20199 finixpnum 28563 upixp 28772 prdstotbnd 28842 |
Copyright terms: Public domain | W3C validator |