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. dffun3
  19. dffun4
  20. dffun5
  21. dffun6f
  22. dffun6
  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. funimaexg
  94. funimaex
  95. isarep1
  96. isarep2
  97. fneq1
  98. fneq2
  99. fneq1d
  100. fneq2d
  101. fneq12d
  102. fneq12
  103. fneq1i
  104. fneq2i
  105. nffn
  106. fnfun
  107. fnfund
  108. fnrel
  109. fndm
  110. fndmi
  111. fndmd
  112. funfni
  113. fndmu
  114. fnbr
  115. fnop
  116. fneu
  117. fneu2
  118. fnun
  119. fnund
  120. fnunop
  121. fncofn
  122. fnco
  123. fncoOLD
  124. fnresdm
  125. fnresdisj
  126. 2elresin
  127. fnssresb
  128. fnssres
  129. fnssresd
  130. fnresin1
  131. fnresin2
  132. fnres
  133. idfn
  134. fnresi
  135. fnresiOLD
  136. fnima
  137. fn0
  138. fnimadisj
  139. fnimaeq0
  140. dfmpt3
  141. mptfnf
  142. fnmptf
  143. fnopabg
  144. fnopab
  145. mptfng
  146. fnmpt
  147. fnmptd
  148. mpt0
  149. fnmpti
  150. dmmpti
  151. dmmptd
  152. mptun
  153. partfun
  154. feq1
  155. feq2
  156. feq3
  157. feq23
  158. feq1d
  159. feq2d
  160. feq3d
  161. feq12d
  162. feq123d
  163. feq123
  164. feq1i
  165. feq2i
  166. feq12i
  167. feq23i
  168. feq23d
  169. nff
  170. sbcfng
  171. sbcfg
  172. elimf
  173. ffn
  174. ffnd
  175. dffn2
  176. ffun
  177. ffund
  178. frel
  179. freld
  180. frn
  181. frnd
  182. fdm
  183. fdmOLD
  184. fdmd
  185. fdmi
  186. dffn3
  187. ffrn
  188. ffrnb
  189. ffrnbd
  190. fss
  191. fssd
  192. fssdmd
  193. fssdm
  194. fimass
  195. fimacnv
  196. fcof
  197. fco
  198. fcoOLD
  199. fcod
  200. fco2
  201. fssxp
  202. funssxp
  203. ffdm
  204. ffdmd
  205. fdmrn
  206. funcofd
  207. fco3OLD
  208. opelf
  209. fun
  210. fun2
  211. fun2d
  212. fnfco
  213. fssres
  214. fssresd
  215. fssres2
  216. fresin
  217. resasplit
  218. fresaun
  219. fresaunres2
  220. fresaunres1
  221. fcoi1
  222. fcoi2
  223. feu
  224. fcnvres
  225. fimacnvdisj
  226. fint
  227. fin
  228. f0
  229. f00
  230. f0bi
  231. f0dom0
  232. f0rn0
  233. fconst
  234. fconstg
  235. fnconstg
  236. fconst6g
  237. fconst6
  238. f1eq1
  239. f1eq2
  240. f1eq3
  241. nff1
  242. dff12
  243. f1f
  244. f1fn
  245. f1fun
  246. f1rel
  247. f1dm
  248. f1dmOLD
  249. f1ss
  250. f1ssr
  251. f1ssres
  252. f1resf1
  253. f1cnvcnv
  254. f1cof1
  255. f1co
  256. f1coOLD
  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. resdif
  310. resin
  311. f1oco
  312. f1cnv
  313. funcocnv2
  314. fococnv2
  315. f1ococnv2
  316. f1cocnv2
  317. f1ococnv1
  318. f1cocnv1
  319. funcoeqres
  320. f1ssf1
  321. f10
  322. f10d
  323. f1o00
  324. fo00
  325. f1o0
  326. f1oi
  327. f1ovi
  328. f1osn
  329. f1osng
  330. f1sng
  331. fsnd
  332. f1oprswap
  333. f1oprg
  334. tz6.12-2
  335. fveu
  336. brprcneu
  337. fvprc
  338. fvprcALT
  339. rnfvprc
  340. fv2
  341. dffv3
  342. dffv4
  343. elfv
  344. fveq1
  345. fveq2
  346. fveq1i
  347. fveq1d
  348. fveq2i
  349. fveq2d
  350. 2fveq3
  351. fveq12i
  352. fveq12d
  353. fveqeq2d
  354. fveqeq2
  355. nffv
  356. nffvmpt1
  357. nffvd
  358. fvex
  359. fvexi
  360. fvexd
  361. fvif
  362. iffv
  363. fv3
  364. fvres
  365. fvresd
  366. funssfv
  367. tz6.12-1
  368. tz6.12
  369. tz6.12f
  370. tz6.12c
  371. tz6.12i
  372. fvbr0
  373. fvrn0
  374. fvssunirn
  375. ndmfv
  376. ndmfvrcl
  377. elfvdm
  378. elfvex
  379. elfvexd
  380. eliman0
  381. nfvres
  382. nfunsn
  383. fvfundmfvn0
  384. 0fv
  385. fv2prc
  386. elfv2ex
  387. fveqres
  388. csbfv12
  389. csbfv2g
  390. csbfv
  391. funbrfv
  392. funopfv
  393. fnbrfvb
  394. fnopfvb
  395. funbrfvb
  396. funopfvb
  397. fnbrfvb2
  398. funbrfv2b
  399. dffn5
  400. fnrnfv
  401. fvelrnb
  402. foelrni
  403. dfimafn
  404. dfimafn2
  405. funimass4
  406. fvelima
  407. fvelimad
  408. feqmptd
  409. feqresmpt
  410. feqmptdf
  411. dffn5f
  412. fvelimab
  413. fvelimabd
  414. unima
  415. fvi
  416. fviss
  417. fniinfv
  418. fnsnfv
  419. fnsnfvOLD
  420. opabiotafun
  421. opabiotadm
  422. opabiota
  423. fnimapr
  424. ssimaex
  425. ssimaexg
  426. funfv
  427. funfv2
  428. funfv2f
  429. fvun
  430. fvun1
  431. fvun2
  432. fvun1d
  433. fvun2d
  434. dffv2
  435. dmfco
  436. fvco2
  437. fvco
  438. fvco3
  439. fvco3d
  440. fvco4i
  441. fvopab3g
  442. fvopab3ig
  443. brfvopabrbr
  444. fvmptg
  445. fvmpti
  446. fvmpt
  447. fvmpt2f
  448. fvtresfn
  449. fvmpts
  450. fvmpt3
  451. fvmpt3i
  452. fvmptdf
  453. fvmptd
  454. fvmptd2
  455. mptrcl
  456. fvmpt2i
  457. fvmpt2
  458. fvmptss
  459. fvmpt2d
  460. fvmptex
  461. fvmptd3f
  462. fvmptd2f
  463. fvmptdv
  464. fvmptdv2
  465. mpteqb
  466. fvmptt
  467. fvmptf
  468. fvmptnf
  469. fvmptd3
  470. fvmptn
  471. fvmptss2
  472. elfvmptrab1w
  473. elfvmptrab1
  474. elfvmptrab
  475. fvopab4ndm
  476. fvmptndm
  477. fvmptrabfv
  478. fvopab5
  479. fvopab6
  480. eqfnfv
  481. eqfnfv2
  482. eqfnfv3
  483. eqfnfvd
  484. eqfnfv2f
  485. eqfunfv
  486. fvreseq0
  487. fvreseq1
  488. fvreseq
  489. fnmptfvd
  490. fndmdif
  491. fndmdifcom
  492. fndmdifeq0
  493. fndmin
  494. fneqeql
  495. fneqeql2
  496. fnreseql
  497. chfnrn
  498. funfvop
  499. funfvbrb
  500. fvimacnvi
  501. fvimacnv
  502. funimass3
  503. funimass5
  504. funconstss
  505. fvimacnvALT
  506. elpreima
  507. elpreimad
  508. fniniseg
  509. fncnvima2
  510. fniniseg2
  511. unpreima
  512. inpreima
  513. difpreima
  514. respreima
  515. cnvimainrn
  516. sspreima
  517. iinpreima
  518. intpreima
  519. fimacnvOLD
  520. fimacnvinrn
  521. fimacnvinrn2
  522. rescnvimafod
  523. fvn0ssdmfun
  524. fnopfv
  525. fvelrn
  526. nelrnfvne
  527. fveqdmss
  528. fveqressseq
  529. fnfvelrn
  530. ffvelrn
  531. ffvelrni
  532. ffvelrnda
  533. ffvelrnd
  534. rexrn
  535. ralrn
  536. elrnrexdm
  537. elrnrexdmb
  538. eldmrexrn
  539. eldmrexrnb
  540. fvcofneq
  541. ralrnmptw
  542. rexrnmptw
  543. ralrnmpt
  544. rexrnmpt
  545. f0cli
  546. dff2
  547. dff3
  548. dff4
  549. dffo3
  550. dffo4
  551. dffo5
  552. exfo
  553. foelrn
  554. foco2
  555. fmpt
  556. f1ompt
  557. fmpti
  558. fvmptelrn
  559. fmptd
  560. fmpttd
  561. fmpt3d
  562. fmptdf
  563. ffnfv
  564. ffnfvf
  565. fnfvrnss
  566. frnssb
  567. rnmptss
  568. fmpt2d
  569. ffvresb
  570. f1oresrab
  571. f1ossf1o
  572. fmptco
  573. fmptcof
  574. fmptcos
  575. cofmpt
  576. fcompt
  577. fcoconst
  578. fsn
  579. fsn2
  580. fsng
  581. fsn2g
  582. xpsng
  583. xpprsng
  584. xpsn
  585. f1o2sn
  586. residpr
  587. dfmpt
  588. fnasrn
  589. idref
  590. funiun
  591. funopsn
  592. funop
  593. funopdmsn
  594. funsndifnop
  595. funsneqopb
  596. ressnop0
  597. fpr
  598. fprg
  599. ftpg
  600. ftp
  601. fnressn
  602. funressn
  603. fressnfv
  604. fvrnressn
  605. fvressn
  606. fvn0fvelrn
  607. fvconst
  608. fnsnr
  609. fnsnb
  610. fmptsn
  611. fmptsng
  612. fmptsnd
  613. fmptap
  614. fmptapd
  615. fmptpr
  616. fvresi
  617. fninfp
  618. fnelfp
  619. fndifnfp
  620. fnelnfp
  621. fnnfpeq0
  622. fvunsn
  623. fvsng
  624. fvsn
  625. fvsnun1
  626. fvsnun2
  627. fnsnsplit
  628. fsnunf
  629. fsnunf2
  630. fsnunfv
  631. fsnunres
  632. funresdfunsn
  633. fvpr1
  634. fvpr2
  635. fvpr1g
  636. fvpr2g
  637. fprb
  638. fvtp1
  639. fvtp2
  640. fvtp3
  641. fvtp1g
  642. fvtp2g
  643. fvtp3g
  644. tpres
  645. fvconst2g
  646. fconst2g
  647. fvconst2
  648. fconst2
  649. fconst5
  650. rnmptc
  651. rnmptcOLD
  652. fnprb
  653. fntpb
  654. fnpr2g
  655. fpr2g
  656. fconstfv
  657. fconst3
  658. fconst4
  659. resfunexg
  660. resiexd
  661. fnex
  662. fnexd
  663. funex
  664. opabex
  665. mptexg
  666. mptexgf
  667. mptex
  668. mptexd
  669. mptrabex
  670. fex
  671. fexd
  672. mptfvmpt
  673. eufnfv
  674. funfvima
  675. funfvima2
  676. funfvima2d
  677. fnfvima
  678. fnfvimad
  679. resfvresima
  680. funfvima3
  681. rexima
  682. ralima
  683. fvclss
  684. elabrex
  685. abrexco
  686. imaiun
  687. imauni
  688. fniunfv
  689. funiunfv
  690. funiunfvf
  691. eluniima
  692. elunirn
  693. elunirnALT
  694. fnunirn
  695. dff13
  696. dff13f
  697. f1veqaeq
  698. f1cofveqaeq
  699. f1cofveqaeqALT
  700. 2f1fvneq
  701. f1mpt
  702. f1fveq
  703. f1elima
  704. f1imass
  705. f1imaeq
  706. f1imapss
  707. fpropnf1
  708. f1dom3fv3dif
  709. f1dom3el3dif
  710. dff14a
  711. dff14b
  712. f12dfv
  713. f13dfv
  714. dff1o6
  715. f1ocnvfv1
  716. f1ocnvfv2
  717. f1ocnvfv
  718. f1ocnvfvb
  719. nvof1o
  720. nvocnv
  721. fsnex
  722. f1prex
  723. f1ocnvdm
  724. f1ocnvfvrneq
  725. fcof1
  726. fcofo
  727. cbvfo
  728. cbvexfo
  729. cocan1
  730. cocan2
  731. fcof1oinvd
  732. fcof1od
  733. 2fcoidinvd
  734. fcof1o
  735. 2fvcoidd
  736. 2fvidf1od
  737. 2fvidinvd
  738. foeqcnvco
  739. f1eqcocnv
  740. f1eqcocnvOLD
  741. fveqf1o
  742. nf1const
  743. nf1oconst
  744. f1ofvswap
  745. fliftrel
  746. fliftel
  747. fliftel1
  748. fliftcnv
  749. fliftfun
  750. fliftfund
  751. fliftfuns
  752. fliftf
  753. fliftval
  754. isoeq1
  755. isoeq2
  756. isoeq3
  757. isoeq4
  758. isoeq5
  759. nfiso
  760. isof1o
  761. isof1oidb
  762. isof1oopb
  763. isorel
  764. soisores
  765. soisoi
  766. isoid
  767. isocnv
  768. isocnv2
  769. isocnv3
  770. isores2
  771. isores1
  772. isores3
  773. isotr
  774. isomin
  775. isoini
  776. isoini2
  777. isofrlem
  778. isoselem
  779. isofr
  780. isose
  781. isofr2
  782. isopolem
  783. isopo
  784. isosolem
  785. isoso
  786. isowe
  787. isowe2
  788. f1oiso
  789. f1oiso2
  790. f1owe
  791. weniso
  792. weisoeq
  793. weisoeq2
  794. knatar