![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fof | Unicode version |
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
fof |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3209 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim2i 342 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fo 5217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-f 5215 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4i 201 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 df-f 5215 df-fo 5217 |
This theorem is referenced by: fofun 5434 fofn 5435 dffo2 5437 foima 5438 resdif 5478 ffoss 5488 fconstfvm 5729 cocan2 5782 foeqcnvco 5784 focdmex 6109 algrflem 6223 algrflemg 6224 tposf2 6262 mapsn 6683 ssdomg 6771 fopwdom 6829 fidcenumlemrks 6945 fidcenumlemr 6947 ctmlemr 7100 ctm 7101 ctssdclemn0 7102 ctssdccl 7103 ctssdc 7105 enumctlemm 7106 enumct 7107 fodjuomnilemdc 7135 exmidfodomrlemr 7194 exmidfodomrlemrALT 7195 suplocexprlemdisj 7697 suplocexprlemub 7700 ennnfonelemdc 12370 ennnfonelemg 12374 ennnfonelemp1 12377 ennnfonelemhdmp1 12380 ennnfonelemkh 12383 ennnfonelemhf1o 12384 ennnfonelemex 12385 ennnfonelemhom 12386 ctinfomlemom 12398 ctinf 12401 ctiunctlemudc 12408 ctiunctlemf 12409 omctfn 12414 mhmid 12855 mhmmnd 12856 mhmfmhm 12857 ghmgrp 12858 dvrecap 13810 subctctexmid 14373 pw1nct 14375 |
Copyright terms: Public domain | W3C validator |