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