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