Metamath Proof Explorer

Table of Contents - 2.3.16. 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. dffun6
  19. dffun3
  20. dffun4
  21. dffun5
  22. dffun6f
  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. fnfund
  108. fnrel
  109. fndm
  110. fndmi
  111. fndmd
  112. funfni
  113. fndmu
  114. fnbr
  115. fnop
  116. fneu
  117. fneu2
  118. fnunres1
  119. fnunres2
  120. fnun
  121. fnund
  122. fnunop
  123. fncofn
  124. fnco
  125. fnresdm
  126. fnresdisj
  127. 2elresin
  128. fnssresb
  129. fnssres
  130. fnssresd
  131. fnresin1
  132. fnresin2
  133. fnres
  134. idfn
  135. fnresi
  136. fnima
  137. fn0
  138. fnimadisj
  139. fnimaeq0
  140. dfmpt3
  141. mptfnf
  142. fnmptf
  143. fnopabg
  144. fnopab
  145. mptfng
  146. fnmpt
  147. fnmptd
  148. mpt0
  149. fnmpti
  150. dmmpti
  151. dmmptd
  152. mptun
  153. partfun
  154. feq1
  155. feq2
  156. feq3
  157. feq23
  158. feq1d
  159. feq1dd
  160. feq2d
  161. feq3d
  162. feq2dd
  163. feq3dd
  164. feq12d
  165. feq123d
  166. feq123
  167. feq1i
  168. feq2i
  169. feq12i
  170. feq23i
  171. feq23d
  172. nff
  173. sbcfng
  174. sbcfg
  175. elimf
  176. ffn
  177. ffnd
  178. dffn2
  179. ffun
  180. ffunOLD
  181. ffund
  182. frel
  183. freld
  184. frn
  185. frnd
  186. fdm
  187. fdmd
  188. fdmi
  189. dffn3
  190. ffrn
  191. ffrnb
  192. ffrnbd
  193. fss
  194. fssd
  195. fssdmd
  196. fssdm
  197. fimass
  198. fimassd
  199. fimacnv
  200. fcof
  201. fco
  202. fcod
  203. fco2
  204. fssxp
  205. funssxp
  206. ffdm
  207. ffdmd
  208. fdmrn
  209. funcofd
  210. opelf
  211. fun
  212. fun2
  213. fun2d
  214. fnfco
  215. fssres
  216. fssresd
  217. fssres2
  218. fresin
  219. resasplit
  220. fresaun
  221. fresaunres2
  222. fresaunres1
  223. fcoi1
  224. fcoi2
  225. feu
  226. fcnvres
  227. fimacnvdisj
  228. fint
  229. fin
  230. f0
  231. f00
  232. f0bi
  233. f0dom0
  234. f0rn0
  235. fconst
  236. fconstg
  237. fnconstg
  238. fconst6g
  239. fconst6
  240. f1eq1
  241. f1eq2
  242. f1eq3
  243. nff1
  244. dff12
  245. f1f
  246. f1fn
  247. f1fun
  248. f1funOLD
  249. f1rel
  250. f1relOLD
  251. f1dm
  252. f1ss
  253. f1ssr
  254. f1ssres
  255. f1resf1
  256. f1cnvcnv
  257. f1cof1
  258. f1co
  259. foeq1
  260. foeq2
  261. foeq3
  262. nffo
  263. fof
  264. fofun
  265. fofn
  266. forn
  267. dffo2
  268. foima
  269. dffn4
  270. funforn
  271. fodmrnu
  272. fimadmfo
  273. fores
  274. fimadmfoALT
  275. focnvimacdmdm
  276. focofo
  277. foco
  278. foconst
  279. f1oeq1
  280. f1oeq2
  281. f1oeq3
  282. f1oeq23
  283. f1eq123d
  284. foeq123d
  285. f1oeq123d
  286. f1oeq1d
  287. f1oeq2d
  288. f1oeq3d
  289. nff1o
  290. f1of1
  291. f1of
  292. f1ofn
  293. f1ofun
  294. f1orel
  295. f1odm
  296. f1odmOLD
  297. dff1o2
  298. dff1o3
  299. f1ofo
  300. dff1o4
  301. dff1o5
  302. f1orn
  303. f1f1orn
  304. f1ocnv
  305. f1ocnvb
  306. f1ores
  307. f1orescnv
  308. f1imacnv
  309. foimacnv
  310. foun
  311. f1oun
  312. f1un
  313. resdif
  314. resin
  315. f1oco
  316. f1cnv
  317. funcocnv2
  318. fococnv2
  319. f1ococnv2
  320. f1cocnv2
  321. f1ococnv1
  322. f1cocnv1
  323. funcoeqres
  324. f1ssf1
  325. f10
  326. f10d
  327. f1o00
  328. fo00
  329. f1o0
  330. f1oi
  331. f1oiOLD
  332. f1ovi
  333. f1osn
  334. f1osng
  335. f1sng
  336. fsnd
  337. f1oprswap
  338. f1oprg
  339. tz6.12-2
  340. tz6.12-2OLD
  341. fveu
  342. brprcneu
  343. brprcneuALT
  344. fvprc
  345. fvprcALT
  346. rnfvprc
  347. fv2
  348. dffv3
  349. dffv4
  350. elfv
  351. fveq1
  352. fveq2
  353. fveq1i
  354. fveq1d
  355. fveq2i
  356. fveq2d
  357. 2fveq3
  358. fveq12i
  359. fveq12d
  360. fveqeq2d
  361. fveqeq2
  362. nffv
  363. nffvmpt1
  364. nffvd
  365. fvex
  366. fvexi
  367. fvexd
  368. fvif
  369. iffv
  370. fv3
  371. fvres
  372. fvresd
  373. funssfv
  374. tz6.12c
  375. tz6.12-1
  376. tz6.12
  377. tz6.12f
  378. tz6.12i
  379. fvbr0
  380. fvrn0
  381. fvn0fvelrn
  382. elfvunirn
  383. fvssunirn
  384. ndmfv
  385. ndmfvrcl
  386. elfvdm
  387. elfvex
  388. elfvexd
  389. eliman0
  390. nfvres
  391. nfunsn
  392. fvfundmfvn0
  393. 0fv
  394. fv2prc
  395. elfv2ex
  396. fveqres
  397. csbfv12
  398. csbfv2g
  399. csbfv
  400. funbrfv
  401. funopfv
  402. fnbrfvb
  403. fnopfvb
  404. fvelima2
  405. funbrfvb
  406. funopfvb
  407. fnbrfvb2
  408. fdmeu
  409. funbrfv2b
  410. dffn5
  411. fnrnfv
  412. fvelrnb
  413. foelcdmi
  414. dfimafn
  415. dfimafn2
  416. funimass4
  417. fvelima
  418. funimassd
  419. fvelimad
  420. feqmptd
  421. feqresmpt
  422. feqmptdf
  423. dffn5f
  424. fvelimab
  425. fvelimabd
  426. fimarab
  427. unima
  428. fvi
  429. fviss
  430. fniinfv
  431. fnsnfv
  432. opabiotafun
  433. opabiotadm
  434. opabiota
  435. fnimapr
  436. fnimatpd
  437. ssimaex
  438. ssimaexg
  439. funfv
  440. funfv2
  441. funfv2f
  442. fvun
  443. fvun1
  444. fvun2
  445. fvun1d
  446. fvun2d
  447. dffv2
  448. dmfco
  449. fvco2
  450. fvco
  451. fvcod
  452. fvco3
  453. fvco3d
  454. fvco4i
  455. fvopab3g
  456. fvopab3ig
  457. brfvopabrbr
  458. fvmptg
  459. fvmpti
  460. fvmpt
  461. fvmpt2f
  462. funcnvmpt
  463. fvtresfn
  464. fvmpts
  465. fvmpt3
  466. fvmpt3i
  467. fvmptdf
  468. fvmptd
  469. fvmptd2
  470. mptrcl
  471. fvmpt2i
  472. fvmpt2
  473. fvmptss
  474. fvmpt2d
  475. fvmptex
  476. fvmptd3f
  477. fvmptd2f
  478. fvmptdv
  479. fvmptdv2
  480. mpteqb
  481. fvmptt
  482. fvmptf
  483. fvmptnf
  484. fvmptd3
  485. fvmptd4
  486. fvmptn
  487. fvmptss2
  488. elfvmptrab1w
  489. elfvmptrab1
  490. elfvmptrab
  491. fvopab4ndm
  492. fvmptndm
  493. fvmptrabfv
  494. fvopab5
  495. fvopab6
  496. eqfnfv
  497. eqfnfv2
  498. eqfnfv3
  499. eqfnfvd
  500. eqfnfv2f
  501. fsneq
  502. eqfunfv
  503. eqfnun
  504. fvreseq0
  505. fvreseq1
  506. fvreseq
  507. fnmptfvd
  508. fndmdif
  509. fndmdifcom
  510. fndmdifeq0
  511. fndmin
  512. fneqeql
  513. fneqeql2
  514. fnreseql
  515. chfnrn
  516. funfvop
  517. funfvbrb
  518. fvimacnvi
  519. fvimacnv
  520. funimass3
  521. funimass5
  522. funconstss
  523. fvimacnvALT
  524. elpreima
  525. elpreimad
  526. fniniseg
  527. fncnvima2
  528. fniniseg2
  529. unpreima
  530. inpreima
  531. difpreima
  532. respreima
  533. cnvimainrn
  534. sspreima
  535. iinpreima
  536. intpreima
  537. fimacnvinrn
  538. fimacnvinrn2
  539. rescnvimafod
  540. fvn0ssdmfun
  541. fnopfv
  542. fvelrn
  543. nelrnfvne
  544. fveqdmss
  545. fveqressseq
  546. fnfvelrn
  547. ffvelcdm
  548. fnfvelrnd
  549. ffvelcdmi
  550. ffvelcdmda
  551. ffvelcdmd
  552. feldmfvelcdm
  553. rexrn
  554. ralrn
  555. elrnrexdm
  556. elrnrexdmb
  557. eldmrexrn
  558. eldmrexrnb
  559. fvcofneq
  560. ralrnmptw
  561. rexrnmptw
  562. ralrnmpt
  563. rexrnmpt
  564. f0cli
  565. dff2
  566. dff3
  567. dff4
  568. dffo3
  569. dffo4
  570. dffo5
  571. exfo
  572. dffo3f
  573. foelrn
  574. foelrnf
  575. foco2
  576. fmpt
  577. f1ompt
  578. fmpti
  579. fvmptelcdm
  580. fmptd
  581. fmpttd
  582. fmpt3d
  583. fmptdf
  584. fompt
  585. ffnfv
  586. ffnfvf
  587. fnfvrnss
  588. fcdmssb
  589. rnmptss
  590. rnmptssd
  591. fmpt2d
  592. ffvresb
  593. fssrescdmd
  594. f1oresrab
  595. f1ossf1o
  596. fmptco
  597. fmptcof
  598. fmptcos
  599. cofmpt
  600. fcompt
  601. fcoconst
  602. fsn
  603. fsn2
  604. fsng
  605. fsn2g
  606. xpsng
  607. xpprsng
  608. xpsn
  609. f1o2sn
  610. residpr
  611. dfmpt
  612. fnasrn
  613. idref
  614. funiun
  615. funopsn
  616. funopsnOLD
  617. funop
  618. funopdmsn
  619. funsndifnop
  620. funsneqopb
  621. ressnop0
  622. fpr
  623. fprg
  624. ftpg
  625. ftp
  626. fnressn
  627. funressn
  628. fressnfv
  629. fvrnressn
  630. fvressn
  631. fvconst
  632. fnsnr
  633. fnsnbg
  634. fnsnb
  635. fnsnbOLD
  636. fmptsn
  637. fmptsng
  638. fmptsnd
  639. fmptap
  640. fmptapd
  641. fmptpr
  642. fvresi
  643. fninfp
  644. fnelfp
  645. fndifnfp
  646. fnelnfp
  647. fnnfpeq0
  648. fvunsn
  649. fvsng
  650. fvsn
  651. fvsnun1
  652. fvsnun2
  653. fnsnsplit
  654. fsnunf
  655. fsnunf2
  656. fsnunfv
  657. fsnunres
  658. funresdfunsn
  659. fvpr1g
  660. fvpr2g
  661. fvpr1
  662. fvpr2
  663. fprb
  664. fvtp1
  665. fvtp2
  666. fvtp3
  667. fvtp1g
  668. fvtp2g
  669. fvtp3g
  670. tpres
  671. fvconst2g
  672. fconst2g
  673. fvconst2
  674. fconst2
  675. fconst5
  676. rnmptc
  677. fnprb
  678. fntpb
  679. fnpr2g
  680. fpr2g
  681. fconstfv
  682. fconst3
  683. fconst4
  684. resfunexg
  685. resiexd
  686. fnex
  687. fnexd
  688. funex
  689. opabex
  690. mptexg
  691. mptexgf
  692. mptex
  693. mptexd
  694. mptrabex
  695. fex
  696. fexd
  697. mptfvmpt
  698. eufnfv
  699. funfvima
  700. funfvima2
  701. funfvima2d
  702. fnfvima
  703. fnfvimad
  704. resfvresima
  705. funfvima3
  706. ralima
  707. rexima
  708. reximaOLD
  709. ralimaOLD
  710. fvclss
  711. elabrex
  712. elabrexg
  713. abrexco
  714. imaiun
  715. imauni
  716. fniunfv
  717. funiunfv
  718. funiunfvf
  719. eluniima
  720. elunirn
  721. elunirnALT
  722. fnunirn
  723. dff13
  724. dff13f
  725. f1veqaeq
  726. f1cofveqaeq
  727. f1cofveqaeqALT
  728. dff14i
  729. 2f1fvneq
  730. f1mpt
  731. f1fveq
  732. f1elima
  733. f1imass
  734. f1imaeq
  735. f1imapss
  736. fpropnf1
  737. f1dom3fv3dif
  738. f1dom3el3dif
  739. dff14a
  740. dff14b
  741. f1ounsn
  742. f12dfv
  743. f13dfv
  744. dff1o6
  745. f1ocnvfv1
  746. f1ocnvfv2
  747. f1ocnvfv
  748. f1ocnvfvb
  749. nvof1o
  750. nvocnv
  751. f1cdmsn
  752. fsnex
  753. f1prex
  754. f1ocnvdm
  755. f1ocnvfvrneq
  756. fcof1
  757. fcofo
  758. cbvfo
  759. cbvexfo
  760. cocan1
  761. cocan2
  762. fcof1oinvd
  763. fcof1od
  764. 2fcoidinvd
  765. fcof1o
  766. 2fvcoidd
  767. 2fvidf1od
  768. 2fvidinvd
  769. foeqcnvco
  770. f1eqcocnv
  771. fveqf1o
  772. f1ocoima
  773. nf1const
  774. nf1oconst
  775. f1ofvswap
  776. fvf1pr
  777. fliftrel
  778. fliftel
  779. fliftel1
  780. fliftcnv
  781. fliftfun
  782. fliftfund
  783. fliftfuns
  784. fliftf
  785. fliftval
  786. isoeq1
  787. isoeq2
  788. isoeq3
  789. isoeq4
  790. isoeq5
  791. nfiso
  792. isof1o
  793. isof1oidb
  794. isof1oopb
  795. isorel
  796. soisores
  797. soisoi
  798. isoid
  799. isocnv
  800. isocnv2
  801. isocnv3
  802. isores2
  803. isores1
  804. isores3
  805. isotr
  806. isomin
  807. isoini
  808. isoini2
  809. isofrlem
  810. isoselem
  811. isofr
  812. isose
  813. isofr2
  814. isopolem
  815. isopo
  816. isosolem
  817. isoso
  818. isowe
  819. isowe2
  820. f1oiso
  821. f1oiso2
  822. f1owe
  823. f1oweOLD
  824. f1we
  825. weniso
  826. weisoeq
  827. weisoeq2
  828. knatar
  829. fvresval
  830. funeldmb
  831. eqfunresadj
  832. eqfunressuc
  833. fnssintima
  834. imaeqsexvOLD
  835. imaeqsalvOLD
  836. fnimasnd