Metamath Proof Explorer

Table of Contents - 2.3.15. Functions

1. wfun
2. wfn
3. wf
4. wf1
5. wfo
6. wf1o
7. cfv
8. wiso
9. df-fun
10. df-fn
11. df-f
12. df-f1
13. df-fo
14. df-f1o
15. df-fv
16. df-isom
17. dffun2
18. dffun3
19. dffun4
20. dffun5
21. dffun6f
22. dffun6
23. funmo
24. funrel
25. 0nelfun
26. funss
27. funeq
28. funeqi
29. funeqd
30. nffun
31. sbcfung
32. funeu
33. funeu2
34. dffun7
35. dffun8
36. dffun9
37. funfn
38. funfnd
39. funi
40. nfunv
41. funopg
42. funopab
43. funopabeq
44. funopab4
45. funmpt
46. funmpt2
47. funco
48. funresfunco
49. funres
50. funresd
51. funssres
52. fun2ssres
53. funun
54. fununmo
55. fununfun
56. fundif
57. funcnvsn
58. funsng
59. fnsng
60. funsn
61. funprg
62. funtpg
63. funpr
64. funtp
65. fnsn
66. fnprg
67. fntpg
68. fntp
69. funcnvpr
70. funcnvtp
71. funcnvqp
72. fun0
73. funcnv0
74. funcnvcnv
75. funcnv2
76. funcnv
77. funcnv3
78. fun2cnv
79. svrelfun
80. fncnv
81. fun11
82. fununi
83. funin
84. funres11
85. funcnvres
86. cnvresid
87. funcnvres2
88. funimacnv
89. funimass1
90. funimass2
91. imadif
92. imain
93. funimaexg
94. funimaex
95. isarep1
96. isarep2
97. fneq1
98. fneq2
99. fneq1d
100. fneq2d
101. fneq12d
102. fneq12
103. fneq1i
104. fneq2i
105. nffn
106. fnfun
107. fnrel
108. fndm
109. fndmi
110. fndmd
111. funfni
112. fndmu
113. fnbr
114. fnop
115. fneu
116. fneu2
117. fnun
118. fnund
119. fnunsn
120. fnco
121. fnresdm
122. fnresdisj
123. 2elresin
124. fnssresb
125. fnssres
126. fnssresd
127. fnresin1
128. fnresin2
129. fnres
130. idfn
131. fnresi
132. fnresiOLD
133. fnima
134. fn0
135. fnimadisj
136. fnimaeq0
137. dfmpt3
138. mptfnf
139. fnmptf
140. fnopabg
141. fnopab
142. mptfng
143. fnmpt
144. fnmptd
145. mpt0
146. fnmpti
147. dmmpti
148. dmmptd
149. mptun
150. partfun
151. feq1
152. feq2
153. feq3
154. feq23
155. feq1d
156. feq2d
157. feq3d
158. feq12d
159. feq123d
160. feq123
161. feq1i
162. feq2i
163. feq12i
164. feq23i
165. feq23d
166. nff
167. sbcfng
168. sbcfg
169. elimf
170. ffn
171. ffnd
172. dffn2
173. ffun
174. ffund
175. frel
176. frn
177. frnd
178. fdm
179. fdmOLD
180. fdmd
181. fdmi
182. dffn3
183. ffrn
184. fss
185. fssd
186. fssdmd
187. fssdm
188. fco
189. fcod
190. fco2
191. fssxp
192. funssxp
193. ffdm
194. ffdmd
195. fdmrn
196. opelf
197. fun
198. fun2
199. fun2d
200. fnfco
201. fssres
202. fssresd
203. fssres2
204. fresin
205. resasplit
206. fresaun
207. fresaunres2
208. fresaunres1
209. fcoi1
210. fcoi2
211. feu
212. fimass
213. fcnvres
214. fimacnvdisj
215. fint
216. fin
217. f0
218. f00
219. f0bi
220. f0dom0
221. f0rn0
222. fconst
223. fconstg
224. fnconstg
225. fconst6g
226. fconst6
227. f1eq1
228. f1eq2
229. f1eq3
230. nff1
231. dff12
232. f1f
233. f1fn
234. f1fun
235. f1rel
236. f1dm
237. f1dmOLD
238. f1ss
239. f1ssr
240. f1ssres
241. f1resf1
242. f1cnvcnv
243. f1co
244. foeq1
245. foeq2
246. foeq3
247. nffo
248. fof
249. fofun
250. fofn
251. forn
252. dffo2
253. foima
254. dffn4
255. funforn
256. fodmrnu
257. fimadmfo
258. fores
259. fimadmfoALT
260. foco
261. foconst
262. f1oeq1
263. f1oeq2
264. f1oeq3
265. f1oeq23
266. f1eq123d
267. foeq123d
268. f1oeq123d
269. f1oeq2d
270. f1oeq3d
271. nff1o
272. f1of1
273. f1of
274. f1ofn
275. f1ofun
276. f1orel
277. f1odm
278. dff1o2
279. dff1o3
280. f1ofo
281. dff1o4
282. dff1o5
283. f1orn
284. f1f1orn
285. f1ocnv
286. f1ocnvb
287. f1ores
288. f1orescnv
289. f1imacnv
290. foimacnv
291. foun
292. f1oun
293. resdif
294. resin
295. f1oco
296. f1cnv
297. funcocnv2
298. fococnv2
299. f1ococnv2
300. f1cocnv2
301. f1ococnv1
302. f1cocnv1
303. funcoeqres
304. f1ssf1
305. f10
306. f10d
307. f1o00
308. fo00
309. f1o0
310. f1oi
311. f1ovi
312. f1osn
313. f1osng
314. f1sng
315. fsnd
316. f1oprswap
317. f1oprg
318. tz6.12-2
319. fveu
320. brprcneu
321. fvprc
322. rnfvprc
323. fv2
324. dffv3
325. dffv4
326. elfv
327. fveq1
328. fveq2
329. fveq1i
330. fveq1d
331. fveq2i
332. fveq2d
333. 2fveq3
334. fveq12i
335. fveq12d
336. fveqeq2d
337. fveqeq2
338. nffv
339. nffvmpt1
340. nffvd
341. fvex
342. fvexi
343. fvexd
344. fvif
345. iffv
346. fv3
347. fvres
348. fvresd
349. funssfv
350. tz6.12-1
351. tz6.12
352. tz6.12f
353. tz6.12c
354. tz6.12i
355. fvbr0
356. fvrn0
357. fvssunirn
358. ndmfv
359. ndmfvrcl
360. elfvdm
361. elfvex
362. elfvexd
363. eliman0
364. nfvres
365. nfunsn
366. fvfundmfvn0
367. 0fv
368. fv2prc
369. elfv2ex
370. fveqres
371. csbfv12
372. csbfv2g
373. csbfv
374. funbrfv
375. funopfv
376. fnbrfvb
377. fnopfvb
378. funbrfvb
379. funopfvb
380. fnbrfvb2
381. funbrfv2b
382. dffn5
383. fnrnfv
384. fvelrnb
385. foelrni
386. dfimafn
387. dfimafn2
388. funimass4
389. fvelima
390. fvelimad
391. feqmptd
392. feqresmpt
393. feqmptdf
394. dffn5f
395. fvelimab
396. fvelimabd
397. unima
398. fvi
399. fviss
400. fniinfv
401. fnsnfv
402. opabiotafun
403. opabiotadm
404. opabiota
405. fnimapr
406. ssimaex
407. ssimaexg
408. funfv
409. funfv2
410. funfv2f
411. fvun
412. fvun1
413. fvun2
414. fvun1d
415. fvun2d
416. dffv2
417. dmfco
418. fvco2
419. fvco
420. fvco3
421. fvco3d
422. fvco4i
423. fvopab3g
424. fvopab3ig
425. brfvopabrbr
426. fvmptg
427. fvmpti
428. fvmpt
429. fvmpt2f
430. fvtresfn
431. fvmpts
432. fvmpt3
433. fvmpt3i
434. fvmptdf
435. fvmptd
436. fvmptd2
437. mptrcl
438. fvmpt2i
439. fvmpt2
440. fvmptss
441. fvmpt2d
442. fvmptex
443. fvmptd3f
444. fvmptd2f
445. fvmptdv
446. fvmptdv2
447. mpteqb
448. fvmptt
449. fvmptf
450. fvmptnf
451. fvmptd3
452. fvmptn
453. fvmptss2
454. elfvmptrab1w
455. elfvmptrab1
456. elfvmptrab
457. fvopab4ndm
458. fvmptndm
459. fvmptrabfv
460. fvopab5
461. fvopab6
462. eqfnfv
463. eqfnfv2
464. eqfnfv3
465. eqfnfvd
466. eqfnfv2f
467. eqfunfv
468. fvreseq0
469. fvreseq1
470. fvreseq
471. fnmptfvd
472. fndmdif
473. fndmdifcom
474. fndmdifeq0
475. fndmin
476. fneqeql
477. fneqeql2
478. fnreseql
479. chfnrn
480. funfvop
481. funfvbrb
482. fvimacnvi
483. fvimacnv
484. funimass3
485. funimass5
486. funconstss
487. fvimacnvALT
488. elpreima
489. elpreimad
490. fniniseg
491. fncnvima2
492. fniniseg2
493. unpreima
494. inpreima
495. difpreima
496. respreima
497. iinpreima
498. intpreima
499. fimacnv
500. fimacnvinrn
501. fimacnvinrn2
502. fvn0ssdmfun
503. fnopfv
504. fvelrn
505. nelrnfvne
506. fveqdmss
507. fveqressseq
508. fnfvelrn
509. ffvelrn
510. ffvelrni
511. ffvelrnda
512. ffvelrnd
513. rexrn
514. ralrn
515. elrnrexdm
516. elrnrexdmb
517. eldmrexrn
518. eldmrexrnb
519. fvcofneq
520. ralrnmptw
521. rexrnmptw
522. ralrnmpt
523. rexrnmpt
524. f0cli
525. dff2
526. dff3
527. dff4
528. dffo3
529. dffo4
530. dffo5
531. exfo
532. foelrn
533. foco2
534. fmpt
535. f1ompt
536. fmpti
537. fvmptelrn
538. fmptd
539. fmpttd
540. fmpt3d
541. fmptdf
542. ffnfv
543. ffnfvf
544. fnfvrnss
545. frnssb
546. rnmptss
547. fmpt2d
548. ffvresb
549. f1oresrab
550. f1ossf1o
551. fmptco
552. fmptcof
553. fmptcos
554. cofmpt
555. fcompt
556. fcoconst
557. fsn
558. fsn2
559. fsng
560. fsn2g
561. xpsng
562. xpprsng
563. xpsn
564. f1o2sn
565. residpr
566. dfmpt
567. fnasrn
568. idref
569. funiun
570. funopsn
571. funop
572. funopdmsn
573. funsndifnop
574. funsneqopb
575. ressnop0
576. fpr
577. fprg
578. ftpg
579. ftp
580. fnressn
581. funressn
582. fressnfv
583. fvrnressn
584. fvressn
585. fvn0fvelrn
586. fvconst
587. fnsnr
588. fnsnb
589. fmptsn
590. fmptsng
591. fmptsnd
592. fmptap
593. fmptapd
594. fmptpr
595. fvresi
596. fninfp
597. fnelfp
598. fndifnfp
599. fnelnfp
600. fnnfpeq0
601. fvunsn
602. fvsng
603. fvsn
604. fvsnun1
605. fvsnun2
606. fnsnsplit
607. fsnunf
608. fsnunf2
609. fsnunfv
610. fsnunres
611. funresdfunsn
612. fvpr1
613. fvpr2
614. fvpr1g
615. fvpr2g
616. fprb
617. fvtp1
618. fvtp2
619. fvtp3
620. fvtp1g
621. fvtp2g
622. fvtp3g
623. tpres
624. fvconst2g
625. fconst2g
626. fvconst2
627. fconst2
628. fconst5
629. rnmptc
630. rnmptcOLD
631. fnprb
632. fntpb
633. fnpr2g
634. fpr2g
635. fconstfv
636. fconst3
637. fconst4
638. resfunexg
639. resiexd
640. fnex
641. fnexd
642. funex
643. opabex
644. mptexg
645. mptexgf
646. mptex
647. mptexd
648. mptrabex
649. fex
650. fexd
651. mptfvmpt
652. eufnfv
653. funfvima
654. funfvima2
655. funfvima2d
656. fnfvima
657. fnfvimad
658. resfvresima
659. funfvima3
660. rexima
661. ralima
662. fvclss
663. elabrex
664. abrexco
665. imaiun
666. imauni
667. fniunfv
668. funiunfv
669. funiunfvf
670. eluniima
671. elunirn
672. elunirnALT
673. fnunirn
674. dff13
675. dff13f
676. f1veqaeq
677. f1cofveqaeq
678. f1cofveqaeqALT
679. 2f1fvneq
680. f1mpt
681. f1fveq
682. f1elima
683. f1imass
684. f1imaeq
685. f1imapss
686. fpropnf1
687. f1dom3fv3dif
688. f1dom3el3dif
689. dff14a
690. dff14b
691. f12dfv
692. f13dfv
693. dff1o6
694. f1ocnvfv1
695. f1ocnvfv2
696. f1ocnvfv
697. f1ocnvfvb
698. nvof1o
699. nvocnv
700. fsnex
701. f1prex
702. f1ocnvdm
703. f1ocnvfvrneq
704. fcof1
705. fcofo
706. cbvfo
707. cbvexfo
708. cocan1
709. cocan2
710. fcof1oinvd
711. fcof1od
712. 2fcoidinvd
713. fcof1o
714. 2fvcoidd
715. 2fvidf1od
716. 2fvidinvd
717. foeqcnvco
718. f1eqcocnv
719. f1eqcocnvOLD
720. fveqf1o
721. nf1const
722. nf1oconst
723. fliftrel
724. fliftel
725. fliftel1
726. fliftcnv
727. fliftfun
728. fliftfund
729. fliftfuns
730. fliftf
731. fliftval
732. isoeq1
733. isoeq2
734. isoeq3
735. isoeq4
736. isoeq5
737. nfiso
738. isof1o
739. isof1oidb
740. isof1oopb
741. isorel
742. soisores
743. soisoi
744. isoid
745. isocnv
746. isocnv2
747. isocnv3
748. isores2
749. isores1
750. isores3
751. isotr
752. isomin
753. isoini
754. isoini2
755. isofrlem
756. isoselem
757. isofr
758. isose
759. isofr2
760. isopolem
761. isopo
762. isosolem
763. isoso
764. isowe
765. isowe2
766. f1oiso
767. f1oiso2
768. f1owe
769. weniso
770. weisoeq
771. weisoeq2
772. knatar