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. fvcod
  449. fvco3
  450. fvco3d
  451. fvco4i
  452. fvopab3g
  453. fvopab3ig
  454. brfvopabrbr
  455. fvmptg
  456. fvmpti
  457. fvmpt
  458. fvmpt2f
  459. funcnvmpt
  460. fvtresfn
  461. fvmpts
  462. fvmpt3
  463. fvmpt3i
  464. fvmptdf
  465. fvmptd
  466. fvmptd2
  467. mptrcl
  468. fvmpt2i
  469. fvmpt2
  470. fvmptss
  471. fvmpt2d
  472. fvmptex
  473. fvmptd3f
  474. fvmptd2f
  475. fvmptdv
  476. fvmptdv2
  477. mpteqb
  478. fvmptt
  479. fvmptf
  480. fvmptnf
  481. fvmptd3
  482. fvmptd4
  483. fvmptn
  484. fvmptss2
  485. elfvmptrab1w
  486. elfvmptrab1
  487. elfvmptrab
  488. fvopab4ndm
  489. fvmptndm
  490. fvmptrabfv
  491. fvopab5
  492. fvopab6
  493. eqfnfv
  494. eqfnfv2
  495. eqfnfv3
  496. eqfnfvd
  497. eqfnfv2f
  498. fsneq
  499. eqfunfv
  500. eqfnun
  501. fvreseq0
  502. fvreseq1
  503. fvreseq
  504. fnmptfvd
  505. fndmdif
  506. fndmdifcom
  507. fndmdifeq0
  508. fndmin
  509. fneqeql
  510. fneqeql2
  511. fnreseql
  512. chfnrn
  513. funfvop
  514. funfvbrb
  515. fvimacnvi
  516. fvimacnv
  517. funimass3
  518. funimass5
  519. funconstss
  520. fvimacnvALT
  521. elpreima
  522. elpreimad
  523. fniniseg
  524. fncnvima2
  525. fniniseg2
  526. unpreima
  527. inpreima
  528. difpreima
  529. respreima
  530. cnvimainrn
  531. sspreima
  532. iinpreima
  533. intpreima
  534. fimacnvinrn
  535. fimacnvinrn2
  536. rescnvimafod
  537. fvn0ssdmfun
  538. fnopfv
  539. fvelrn
  540. nelrnfvne
  541. fveqdmss
  542. fveqressseq
  543. fnfvelrn
  544. ffvelcdm
  545. fnfvelrnd
  546. ffvelcdmi
  547. ffvelcdmda
  548. ffvelcdmd
  549. feldmfvelcdm
  550. rexrn
  551. ralrn
  552. elrnrexdm
  553. elrnrexdmb
  554. eldmrexrn
  555. eldmrexrnb
  556. fvcofneq
  557. ralrnmptw
  558. rexrnmptw
  559. ralrnmpt
  560. rexrnmpt
  561. f0cli
  562. dff2
  563. dff3
  564. dff4
  565. dffo3
  566. dffo4
  567. dffo5
  568. exfo
  569. dffo3f
  570. foelrn
  571. foelrnf
  572. foco2
  573. fmpt
  574. f1ompt
  575. fmpti
  576. fvmptelcdm
  577. fmptd
  578. fmpttd
  579. fmpt3d
  580. fmptdf
  581. fompt
  582. ffnfv
  583. ffnfvf
  584. fnfvrnss
  585. fcdmssb
  586. rnmptss
  587. rnmptssd
  588. fmpt2d
  589. ffvresb
  590. fssrescdmd
  591. f1oresrab
  592. f1ossf1o
  593. fmptco
  594. fmptcof
  595. fmptcos
  596. cofmpt
  597. fcompt
  598. fcoconst
  599. fsn
  600. fsn2
  601. fsng
  602. fsn2g
  603. xpsng
  604. xpprsng
  605. xpsn
  606. f1o2sn
  607. residpr
  608. dfmpt
  609. fnasrn
  610. idref
  611. funiun
  612. funopsn
  613. funopsnOLD
  614. funop
  615. funopdmsn
  616. funsndifnop
  617. funsneqopb
  618. ressnop0
  619. fpr
  620. fprg
  621. ftpg
  622. ftp
  623. fnressn
  624. funressn
  625. fressnfv
  626. fvrnressn
  627. fvressn
  628. fvconst
  629. fnsnr
  630. fnsnbg
  631. fnsnb
  632. fnsnbOLD
  633. fmptsn
  634. fmptsng
  635. fmptsnd
  636. fmptap
  637. fmptapd
  638. fmptpr
  639. fvresi
  640. fninfp
  641. fnelfp
  642. fndifnfp
  643. fnelnfp
  644. fnnfpeq0
  645. fvunsn
  646. fvsng
  647. fvsn
  648. fvsnun1
  649. fvsnun2
  650. fnsnsplit
  651. fsnunf
  652. fsnunf2
  653. fsnunfv
  654. fsnunres
  655. funresdfunsn
  656. fvpr1g
  657. fvpr2g
  658. fvpr1
  659. fvpr2
  660. fprb
  661. fvtp1
  662. fvtp2
  663. fvtp3
  664. fvtp1g
  665. fvtp2g
  666. fvtp3g
  667. tpres
  668. fvconst2g
  669. fconst2g
  670. fvconst2
  671. fconst2
  672. fconst5
  673. rnmptc
  674. fnprb
  675. fntpb
  676. fnpr2g
  677. fpr2g
  678. fconstfv
  679. fconst3
  680. fconst4
  681. resfunexg
  682. resiexd
  683. fnex
  684. fnexd
  685. funex
  686. opabex
  687. mptexg
  688. mptexgf
  689. mptex
  690. mptexd
  691. mptrabex
  692. fex
  693. fexd
  694. mptfvmpt
  695. eufnfv
  696. funfvima
  697. funfvima2
  698. funfvima2d
  699. fnfvima
  700. fnfvimad
  701. resfvresima
  702. funfvima3
  703. ralima
  704. rexima
  705. reximaOLD
  706. ralimaOLD
  707. fvclss
  708. elabrex
  709. elabrexg
  710. abrexco
  711. imaiun
  712. imauni
  713. fniunfv
  714. funiunfv
  715. funiunfvf
  716. eluniima
  717. elunirn
  718. elunirnALT
  719. fnunirn
  720. dff13
  721. dff13f
  722. f1veqaeq
  723. f1cofveqaeq
  724. f1cofveqaeqALT
  725. dff14i
  726. 2f1fvneq
  727. f1mpt
  728. f1fveq
  729. f1elima
  730. f1imass
  731. f1imaeq
  732. f1imapss
  733. fpropnf1
  734. f1dom3fv3dif
  735. f1dom3el3dif
  736. dff14a
  737. dff14b
  738. f1ounsn
  739. f12dfv
  740. f13dfv
  741. dff1o6
  742. f1ocnvfv1
  743. f1ocnvfv2
  744. f1ocnvfv
  745. f1ocnvfvb
  746. nvof1o
  747. nvocnv
  748. f1cdmsn
  749. fsnex
  750. f1prex
  751. f1ocnvdm
  752. f1ocnvfvrneq
  753. fcof1
  754. fcofo
  755. cbvfo
  756. cbvexfo
  757. cocan1
  758. cocan2
  759. fcof1oinvd
  760. fcof1od
  761. 2fcoidinvd
  762. fcof1o
  763. 2fvcoidd
  764. 2fvidf1od
  765. 2fvidinvd
  766. foeqcnvco
  767. f1eqcocnv
  768. fveqf1o
  769. f1ocoima
  770. nf1const
  771. nf1oconst
  772. f1ofvswap
  773. fvf1pr
  774. fliftrel
  775. fliftel
  776. fliftel1
  777. fliftcnv
  778. fliftfun
  779. fliftfund
  780. fliftfuns
  781. fliftf
  782. fliftval
  783. isoeq1
  784. isoeq2
  785. isoeq3
  786. isoeq4
  787. isoeq5
  788. nfiso
  789. isof1o
  790. isof1oidb
  791. isof1oopb
  792. isorel
  793. soisores
  794. soisoi
  795. isoid
  796. isocnv
  797. isocnv2
  798. isocnv3
  799. isores2
  800. isores1
  801. isores3
  802. isotr
  803. isomin
  804. isoini
  805. isoini2
  806. isofrlem
  807. isoselem
  808. isofr
  809. isose
  810. isofr2
  811. isopolem
  812. isopo
  813. isosolem
  814. isoso
  815. isowe
  816. isowe2
  817. f1oiso
  818. f1oiso2
  819. f1owe
  820. weniso
  821. weisoeq
  822. weisoeq2
  823. knatar
  824. fvresval
  825. funeldmb
  826. eqfunresadj
  827. eqfunressuc
  828. fnssintima
  829. imaeqsexvOLD
  830. imaeqsalvOLD
  831. fnimasnd