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. f1imadifssran
  99. funimaexg
  100. funimaexgOLD
  101. funimaex
  102. isarep1
  103. isarep1OLD
  104. isarep2
  105. fneq1
  106. fneq2
  107. fneq1d
  108. fneq2d
  109. fneq12d
  110. fneq12
  111. fneq1i
  112. fneq2i
  113. nffn
  114. fnfun
  115. fnfund
  116. fnrel
  117. fndm
  118. fndmi
  119. fndmd
  120. funfni
  121. fndmu
  122. fnbr
  123. fnop
  124. fneu
  125. fneu2
  126. fnunres1
  127. fnunres2
  128. fnun
  129. fnund
  130. fnunop
  131. fncofn
  132. fnco
  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. feq1dd
  168. feq2d
  169. feq3d
  170. feq2dd
  171. feq3dd
  172. feq12d
  173. feq123d
  174. feq123
  175. feq1i
  176. feq2i
  177. feq12i
  178. feq23i
  179. feq23d
  180. nff
  181. sbcfng
  182. sbcfg
  183. elimf
  184. ffn
  185. ffnd
  186. dffn2
  187. ffun
  188. ffund
  189. frel
  190. freld
  191. frn
  192. frnd
  193. fdm
  194. fdmd
  195. fdmi
  196. dffn3
  197. ffrn
  198. ffrnb
  199. ffrnbd
  200. fss
  201. fssd
  202. fssdmd
  203. fssdm
  204. fimass
  205. fimassd
  206. fimacnv
  207. fcof
  208. fco
  209. fcod
  210. fco2
  211. fssxp
  212. funssxp
  213. ffdm
  214. ffdmd
  215. fdmrn
  216. funcofd
  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. f1ss
  258. f1ssr
  259. f1ssres
  260. f1resf1
  261. f1cnvcnv
  262. f1cof1
  263. f1co
  264. foeq1
  265. foeq2
  266. foeq3
  267. nffo
  268. fof
  269. fofun
  270. fofn
  271. forn
  272. dffo2
  273. foima
  274. dffn4
  275. funforn
  276. fodmrnu
  277. fimadmfo
  278. fores
  279. fimadmfoALT
  280. focnvimacdmdm
  281. focofo
  282. foco
  283. foconst
  284. f1oeq1
  285. f1oeq2
  286. f1oeq3
  287. f1oeq23
  288. f1eq123d
  289. foeq123d
  290. f1oeq123d
  291. f1oeq1d
  292. f1oeq2d
  293. f1oeq3d
  294. nff1o
  295. f1of1
  296. f1of
  297. f1ofn
  298. f1ofun
  299. f1orel
  300. f1odm
  301. dff1o2
  302. dff1o3
  303. f1ofo
  304. dff1o4
  305. dff1o5
  306. f1orn
  307. f1f1orn
  308. f1ocnv
  309. f1ocnvb
  310. f1ores
  311. f1orescnv
  312. f1imacnv
  313. foimacnv
  314. foun
  315. f1oun
  316. f1un
  317. resdif
  318. resin
  319. f1oco
  320. f1cnv
  321. funcocnv2
  322. fococnv2
  323. f1ococnv2
  324. f1cocnv2
  325. f1ococnv1
  326. f1cocnv1
  327. funcoeqres
  328. f1ssf1
  329. f10
  330. f10d
  331. f1o00
  332. fo00
  333. f1o0
  334. f1oi
  335. f1ovi
  336. f1osn
  337. f1osng
  338. f1sng
  339. fsnd
  340. f1oprswap
  341. f1oprg
  342. tz6.12-2
  343. fveu
  344. brprcneu
  345. brprcneuALT
  346. fvprc
  347. fvprcALT
  348. rnfvprc
  349. fv2
  350. dffv3
  351. dffv4
  352. elfv
  353. fveq1
  354. fveq2
  355. fveq1i
  356. fveq1d
  357. fveq2i
  358. fveq2d
  359. 2fveq3
  360. fveq12i
  361. fveq12d
  362. fveqeq2d
  363. fveqeq2
  364. nffv
  365. nffvmpt1
  366. nffvd
  367. fvex
  368. fvexi
  369. fvexd
  370. fvif
  371. iffv
  372. fv3
  373. fvres
  374. fvresd
  375. funssfv
  376. tz6.12c
  377. tz6.12-1
  378. tz6.12-1OLD
  379. tz6.12
  380. tz6.12f
  381. tz6.12cOLD
  382. tz6.12i
  383. fvbr0
  384. fvrn0
  385. fvn0fvelrn
  386. elfvunirn
  387. fvssunirn
  388. fvssunirnOLD
  389. ndmfv
  390. ndmfvrcl
  391. elfvdm
  392. elfvex
  393. elfvexd
  394. eliman0
  395. nfvres
  396. nfunsn
  397. fvfundmfvn0
  398. 0fv
  399. fv2prc
  400. elfv2ex
  401. fveqres
  402. csbfv12
  403. csbfv2g
  404. csbfv
  405. funbrfv
  406. funopfv
  407. fnbrfvb
  408. fnopfvb
  409. fvelima2
  410. funbrfvb
  411. funopfvb
  412. fnbrfvb2
  413. fdmeu
  414. funbrfv2b
  415. dffn5
  416. fnrnfv
  417. fvelrnb
  418. foelcdmi
  419. dfimafn
  420. dfimafn2
  421. funimass4
  422. fvelima
  423. funimassd
  424. fvelimad
  425. feqmptd
  426. feqresmpt
  427. feqmptdf
  428. dffn5f
  429. fvelimab
  430. fvelimabd
  431. fimarab
  432. unima
  433. fvi
  434. fviss
  435. fniinfv
  436. fnsnfv
  437. opabiotafun
  438. opabiotadm
  439. opabiota
  440. fnimapr
  441. fnimatpd
  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. fimacnvinrn
  540. fimacnvinrn2
  541. rescnvimafod
  542. fvn0ssdmfun
  543. fnopfv
  544. fvelrn
  545. nelrnfvne
  546. fveqdmss
  547. fveqressseq
  548. fnfvelrn
  549. ffvelcdm
  550. fnfvelrnd
  551. ffvelcdmi
  552. ffvelcdmda
  553. ffvelcdmd
  554. feldmfvelcdm
  555. rexrn
  556. ralrn
  557. elrnrexdm
  558. elrnrexdmb
  559. eldmrexrn
  560. eldmrexrnb
  561. fvcofneq
  562. ralrnmptw
  563. rexrnmptw
  564. ralrnmpt
  565. rexrnmpt
  566. f0cli
  567. dff2
  568. dff3
  569. dff4
  570. dffo3
  571. dffo4
  572. dffo5
  573. exfo
  574. dffo3f
  575. foelrn
  576. foelrnf
  577. foco2
  578. fmpt
  579. f1ompt
  580. fmpti
  581. fvmptelcdm
  582. fmptd
  583. fmpttd
  584. fmpt3d
  585. fmptdf
  586. fompt
  587. ffnfv
  588. ffnfvf
  589. fnfvrnss
  590. fcdmssb
  591. rnmptss
  592. fmpt2d
  593. ffvresb
  594. fssrescdmd
  595. f1oresrab
  596. f1ossf1o
  597. fmptco
  598. fmptcof
  599. fmptcos
  600. cofmpt
  601. fcompt
  602. fcoconst
  603. fsn
  604. fsn2
  605. fsng
  606. fsn2g
  607. xpsng
  608. xpprsng
  609. xpsn
  610. f1o2sn
  611. residpr
  612. dfmpt
  613. fnasrn
  614. idref
  615. funiun
  616. funopsn
  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. fvn0fvelrnOLD
  632. fvconst
  633. fnsnr
  634. fnsnbg
  635. fnsnb
  636. fnsnbOLD
  637. fmptsn
  638. fmptsng
  639. fmptsnd
  640. fmptap
  641. fmptapd
  642. fmptpr
  643. fvresi
  644. fninfp
  645. fnelfp
  646. fndifnfp
  647. fnelnfp
  648. fnnfpeq0
  649. fvunsn
  650. fvsng
  651. fvsn
  652. fvsnun1
  653. fvsnun2
  654. fnsnsplit
  655. fsnunf
  656. fsnunf2
  657. fsnunfv
  658. fsnunres
  659. funresdfunsn
  660. fvpr1g
  661. fvpr2g
  662. fvpr1
  663. fvpr2
  664. fprb
  665. fvtp1
  666. fvtp2
  667. fvtp3
  668. fvtp1g
  669. fvtp2g
  670. fvtp3g
  671. tpres
  672. fvconst2g
  673. fconst2g
  674. fvconst2
  675. fconst2
  676. fconst5
  677. rnmptc
  678. fnprb
  679. fntpb
  680. fnpr2g
  681. fpr2g
  682. fconstfv
  683. fconst3
  684. fconst4
  685. resfunexg
  686. resiexd
  687. fnex
  688. fnexd
  689. funex
  690. opabex
  691. mptexg
  692. mptexgf
  693. mptex
  694. mptexd
  695. mptrabex
  696. fex
  697. fexd
  698. mptfvmpt
  699. eufnfv
  700. funfvima
  701. funfvima2
  702. funfvima2d
  703. fnfvima
  704. fnfvimad
  705. resfvresima
  706. funfvima3
  707. ralima
  708. rexima
  709. reximaOLD
  710. ralimaOLD
  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. dff14i
  731. 2f1fvneq
  732. f1mpt
  733. f1fveq
  734. f1elima
  735. f1imass
  736. f1imaeq
  737. f1imapss
  738. fpropnf1
  739. f1dom3fv3dif
  740. f1dom3el3dif
  741. dff14a
  742. dff14b
  743. f1ounsn
  744. f12dfv
  745. f13dfv
  746. dff1o6
  747. f1ocnvfv1
  748. f1ocnvfv2
  749. f1ocnvfv
  750. f1ocnvfvb
  751. nvof1o
  752. nvocnv
  753. f1cdmsn
  754. fsnex
  755. f1prex
  756. f1ocnvdm
  757. f1ocnvfvrneq
  758. fcof1
  759. fcofo
  760. cbvfo
  761. cbvexfo
  762. cocan1
  763. cocan2
  764. fcof1oinvd
  765. fcof1od
  766. 2fcoidinvd
  767. fcof1o
  768. 2fvcoidd
  769. 2fvidf1od
  770. 2fvidinvd
  771. foeqcnvco
  772. f1eqcocnv
  773. fveqf1o
  774. f1ocoima
  775. nf1const
  776. nf1oconst
  777. f1ofvswap
  778. fvf1pr
  779. fliftrel
  780. fliftel
  781. fliftel1
  782. fliftcnv
  783. fliftfun
  784. fliftfund
  785. fliftfuns
  786. fliftf
  787. fliftval
  788. isoeq1
  789. isoeq2
  790. isoeq3
  791. isoeq4
  792. isoeq5
  793. nfiso
  794. isof1o
  795. isof1oidb
  796. isof1oopb
  797. isorel
  798. soisores
  799. soisoi
  800. isoid
  801. isocnv
  802. isocnv2
  803. isocnv3
  804. isores2
  805. isores1
  806. isores3
  807. isotr
  808. isomin
  809. isoini
  810. isoini2
  811. isofrlem
  812. isoselem
  813. isofr
  814. isose
  815. isofr2
  816. isopolem
  817. isopo
  818. isosolem
  819. isoso
  820. isowe
  821. isowe2
  822. f1oiso
  823. f1oiso2
  824. f1owe
  825. weniso
  826. weisoeq
  827. weisoeq2
  828. knatar
  829. fvresval
  830. funeldmb
  831. eqfunresadj
  832. eqfunressuc
  833. fnssintima
  834. imaeqsexvOLD
  835. imaeqsalvOLD
  836. fnimasnd