![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ffnfv | Structured version Visualization version Unicode version |
Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
Ref | Expression |
---|---|
ffnfv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5751 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ffvelrn 6043 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | ralrimiva 2814 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | jca 539 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | simpl 463 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | fvelrnb 5935 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | biimpd 212 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | nfra1 2781 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | nfv 1772 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() | |
10 | rsp 2766 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | eleq1 2528 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | 11 | biimpcd 232 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 10, 12 | syl6 34 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 8, 9, 13 | rexlimd 2883 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 7, 14 | sylan9 667 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15 | ssrdv 3450 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | df-f 5605 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 5, 16, 17 | sylanbrc 675 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 4, 18 | impbii 192 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-fv 5609 |
This theorem is referenced by: ffnfvf 6073 fnfvrnss 6074 frnssb 6075 fmpt2d 6077 fconstfv 6151 ffnov 6427 seqomlem2 7194 elixpconst 7556 elixpsn 7587 unblem4 7852 ordtypelem4 8062 oismo 8081 cantnfvalf 8196 rankf 8291 alephon 8526 alephf1 8542 alephf1ALT 8560 alephfplem4 8564 cfsmolem 8726 infpssrlem3 8761 axcc4 8895 domtriomlem 8898 axdclem2 8976 pwfseqlem3 9111 gch3 9127 inar1 9226 peano5nni 10640 cnref1o 11326 seqf2 12264 hashkf 12549 iswrdsymb 12720 ccatrn 12769 shftf 13191 sqrtf 13475 isercoll2 13781 eff2 14202 reeff1 14223 1arith 14920 ramcl 15036 xpscf 15521 dmaf 15993 cdaf 15994 coapm 16015 odf 17235 odfOLD 17251 gsumpt 17643 dprdff 17694 dprdfcntz 17697 dprdfadd 17702 dprdlub 17708 mgpf 17841 prdscrngd 17890 isabvd 18097 psrbagcon 18644 subrgmvrf 18735 mplbas2 18743 mvrf2 18764 psgnghm 19197 frlmsslsp 19403 kqf 20811 fmf 21009 tmdgsum2 21160 prdstmdd 21187 prdstgpd 21188 prdsxmslem2 21593 metdsre 21919 metdsreOLD 21934 evth 22036 evthicc2 22460 ovolfsf 22473 ovolf 22484 vitalilem2 22616 vitalilem5 22619 0plef 22679 mbfi1fseqlem4 22725 xrge0f 22738 itg2addlem 22765 dvfre 22954 dvne0 23012 mdegxrf 23066 mtest 23408 psercn 23430 recosf1o 23533 logcn 23641 amgm 23965 emcllem7 23976 dchrfi 24232 dchr1re 24240 dchrisum0re 24400 padicabvf 24518 hlimf 26939 pjrni 27404 pjmf1 27418 bnj149 29735 subfacp1lem3 29954 mrsubrn 30200 msrf 30229 mclsind 30257 neibastop2lem 31065 rrncmslem 32209 cdlemk56 34583 hbtlem7 36029 dgraaf 36056 dgraafOLD 36057 deg1mhm 36129 resincncf 37790 dvnprodlem1 37859 qndenserrnbllem 38201 fge0iccico 38250 elhoi 38402 ovnsubaddlem1 38430 hoiqssbllem3 38484 vtxdgfisf 39586 |
Copyright terms: Public domain | W3C validator |