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