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. f1ovi
  329. f1osn
  330. f1osng
  331. f1sng
  332. fsnd
  333. f1oprswap
  334. f1oprg
  335. tz6.12-2
  336. fveu
  337. brprcneu
  338. brprcneuALT
  339. fvprc
  340. fvprcALT
  341. rnfvprc
  342. fv2
  343. dffv3
  344. dffv4
  345. elfv
  346. fveq1
  347. fveq2
  348. fveq1i
  349. fveq1d
  350. fveq2i
  351. fveq2d
  352. 2fveq3
  353. fveq12i
  354. fveq12d
  355. fveqeq2d
  356. fveqeq2
  357. nffv
  358. nffvmpt1
  359. nffvd
  360. fvex
  361. fvexi
  362. fvexd
  363. fvif
  364. iffv
  365. fv3
  366. fvres
  367. fvresd
  368. funssfv
  369. tz6.12c
  370. tz6.12-1
  371. tz6.12
  372. tz6.12f
  373. tz6.12i
  374. fvbr0
  375. fvrn0
  376. fvn0fvelrn
  377. elfvunirn
  378. fvssunirn
  379. fvssunirnOLD
  380. ndmfv
  381. ndmfvrcl
  382. elfvdm
  383. elfvex
  384. elfvexd
  385. eliman0
  386. nfvres
  387. nfunsn
  388. fvfundmfvn0
  389. 0fv
  390. fv2prc
  391. elfv2ex
  392. fveqres
  393. csbfv12
  394. csbfv2g
  395. csbfv
  396. funbrfv
  397. funopfv
  398. fnbrfvb
  399. fnopfvb
  400. fvelima2
  401. funbrfvb
  402. funopfvb
  403. fnbrfvb2
  404. fdmeu
  405. funbrfv2b
  406. dffn5
  407. fnrnfv
  408. fvelrnb
  409. foelcdmi
  410. dfimafn
  411. dfimafn2
  412. funimass4
  413. fvelima
  414. funimassd
  415. fvelimad
  416. feqmptd
  417. feqresmpt
  418. feqmptdf
  419. dffn5f
  420. fvelimab
  421. fvelimabd
  422. fimarab
  423. unima
  424. fvi
  425. fviss
  426. fniinfv
  427. fnsnfv
  428. opabiotafun
  429. opabiotadm
  430. opabiota
  431. fnimapr
  432. fnimatpd
  433. ssimaex
  434. ssimaexg
  435. funfv
  436. funfv2
  437. funfv2f
  438. fvun
  439. fvun1
  440. fvun2
  441. fvun1d
  442. fvun2d
  443. dffv2
  444. dmfco
  445. fvco2
  446. fvco
  447. fvco3
  448. fvco3d
  449. fvco4i
  450. fvopab3g
  451. fvopab3ig
  452. brfvopabrbr
  453. fvmptg
  454. fvmpti
  455. fvmpt
  456. fvmpt2f
  457. fvtresfn
  458. fvmpts
  459. fvmpt3
  460. fvmpt3i
  461. fvmptdf
  462. fvmptd
  463. fvmptd2
  464. mptrcl
  465. fvmpt2i
  466. fvmpt2
  467. fvmptss
  468. fvmpt2d
  469. fvmptex
  470. fvmptd3f
  471. fvmptd2f
  472. fvmptdv
  473. fvmptdv2
  474. mpteqb
  475. fvmptt
  476. fvmptf
  477. fvmptnf
  478. fvmptd3
  479. fvmptd4
  480. fvmptn
  481. fvmptss2
  482. elfvmptrab1w
  483. elfvmptrab1
  484. elfvmptrab
  485. fvopab4ndm
  486. fvmptndm
  487. fvmptrabfv
  488. fvopab5
  489. fvopab6
  490. eqfnfv
  491. eqfnfv2
  492. eqfnfv3
  493. eqfnfvd
  494. eqfnfv2f
  495. eqfunfv
  496. eqfnun
  497. fvreseq0
  498. fvreseq1
  499. fvreseq
  500. fnmptfvd
  501. fndmdif
  502. fndmdifcom
  503. fndmdifeq0
  504. fndmin
  505. fneqeql
  506. fneqeql2
  507. fnreseql
  508. chfnrn
  509. funfvop
  510. funfvbrb
  511. fvimacnvi
  512. fvimacnv
  513. funimass3
  514. funimass5
  515. funconstss
  516. fvimacnvALT
  517. elpreima
  518. elpreimad
  519. fniniseg
  520. fncnvima2
  521. fniniseg2
  522. unpreima
  523. inpreima
  524. difpreima
  525. respreima
  526. cnvimainrn
  527. sspreima
  528. iinpreima
  529. intpreima
  530. fimacnvinrn
  531. fimacnvinrn2
  532. rescnvimafod
  533. fvn0ssdmfun
  534. fnopfv
  535. fvelrn
  536. nelrnfvne
  537. fveqdmss
  538. fveqressseq
  539. fnfvelrn
  540. ffvelcdm
  541. fnfvelrnd
  542. ffvelcdmi
  543. ffvelcdmda
  544. ffvelcdmd
  545. feldmfvelcdm
  546. rexrn
  547. ralrn
  548. elrnrexdm
  549. elrnrexdmb
  550. eldmrexrn
  551. eldmrexrnb
  552. fvcofneq
  553. ralrnmptw
  554. rexrnmptw
  555. ralrnmpt
  556. rexrnmpt
  557. f0cli
  558. dff2
  559. dff3
  560. dff4
  561. dffo3
  562. dffo4
  563. dffo5
  564. exfo
  565. dffo3f
  566. foelrn
  567. foelrnf
  568. foco2
  569. fmpt
  570. f1ompt
  571. fmpti
  572. fvmptelcdm
  573. fmptd
  574. fmpttd
  575. fmpt3d
  576. fmptdf
  577. fompt
  578. ffnfv
  579. ffnfvf
  580. fnfvrnss
  581. fcdmssb
  582. rnmptss
  583. fmpt2d
  584. ffvresb
  585. fssrescdmd
  586. f1oresrab
  587. f1ossf1o
  588. fmptco
  589. fmptcof
  590. fmptcos
  591. cofmpt
  592. fcompt
  593. fcoconst
  594. fsn
  595. fsn2
  596. fsng
  597. fsn2g
  598. xpsng
  599. xpprsng
  600. xpsn
  601. f1o2sn
  602. residpr
  603. dfmpt
  604. fnasrn
  605. idref
  606. funiun
  607. funopsn
  608. funop
  609. funopdmsn
  610. funsndifnop
  611. funsneqopb
  612. ressnop0
  613. fpr
  614. fprg
  615. ftpg
  616. ftp
  617. fnressn
  618. funressn
  619. fressnfv
  620. fvrnressn
  621. fvressn
  622. fvn0fvelrnOLD
  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. elunirn2OLD
  715. fnunirn
  716. dff13
  717. dff13f
  718. f1veqaeq
  719. f1cofveqaeq
  720. f1cofveqaeqALT
  721. dff14i
  722. 2f1fvneq
  723. f1mpt
  724. f1fveq
  725. f1elima
  726. f1imass
  727. f1imaeq
  728. f1imapss
  729. fpropnf1
  730. f1dom3fv3dif
  731. f1dom3el3dif
  732. dff14a
  733. dff14b
  734. f1ounsn
  735. f12dfv
  736. f13dfv
  737. dff1o6
  738. f1ocnvfv1
  739. f1ocnvfv2
  740. f1ocnvfv
  741. f1ocnvfvb
  742. nvof1o
  743. nvocnv
  744. f1cdmsn
  745. fsnex
  746. f1prex
  747. f1ocnvdm
  748. f1ocnvfvrneq
  749. fcof1
  750. fcofo
  751. cbvfo
  752. cbvexfo
  753. cocan1
  754. cocan2
  755. fcof1oinvd
  756. fcof1od
  757. 2fcoidinvd
  758. fcof1o
  759. 2fvcoidd
  760. 2fvidf1od
  761. 2fvidinvd
  762. foeqcnvco
  763. f1eqcocnv
  764. fveqf1o
  765. f1ocoima
  766. nf1const
  767. nf1oconst
  768. f1ofvswap
  769. fvf1pr
  770. fliftrel
  771. fliftel
  772. fliftel1
  773. fliftcnv
  774. fliftfun
  775. fliftfund
  776. fliftfuns
  777. fliftf
  778. fliftval
  779. isoeq1
  780. isoeq2
  781. isoeq3
  782. isoeq4
  783. isoeq5
  784. nfiso
  785. isof1o
  786. isof1oidb
  787. isof1oopb
  788. isorel
  789. soisores
  790. soisoi
  791. isoid
  792. isocnv
  793. isocnv2
  794. isocnv3
  795. isores2
  796. isores1
  797. isores3
  798. isotr
  799. isomin
  800. isoini
  801. isoini2
  802. isofrlem
  803. isoselem
  804. isofr
  805. isose
  806. isofr2
  807. isopolem
  808. isopo
  809. isosolem
  810. isoso
  811. isowe
  812. isowe2
  813. f1oiso
  814. f1oiso2
  815. f1owe
  816. weniso
  817. weisoeq
  818. weisoeq2
  819. knatar
  820. fvresval
  821. funeldmb
  822. eqfunresadj
  823. eqfunressuc
  824. fnssintima
  825. imaeqsexvOLD
  826. imaeqsalvOLD
  827. fnimasnd