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. brprcneuALT
  338. fvprc
  339. fvprcALT
  340. rnfvprc
  341. fv2
  342. dffv3
  343. dffv4
  344. elfv
  345. fveq1
  346. fveq2
  347. fveq1i
  348. fveq1d
  349. fveq2i
  350. fveq2d
  351. 2fveq3
  352. fveq12i
  353. fveq12d
  354. fveqeq2d
  355. fveqeq2
  356. nffv
  357. nffvmpt1
  358. nffvd
  359. fvex
  360. fvexi
  361. fvexd
  362. fvif
  363. iffv
  364. fv3
  365. fvres
  366. fvresd
  367. funssfv
  368. tz6.12-1
  369. tz6.12
  370. tz6.12f
  371. tz6.12c
  372. tz6.12i
  373. fvbr0
  374. fvrn0
  375. fvssunirn
  376. ndmfv
  377. ndmfvrcl
  378. elfvdm
  379. elfvex
  380. elfvexd
  381. eliman0
  382. nfvres
  383. nfunsn
  384. fvfundmfvn0
  385. 0fv
  386. fv2prc
  387. elfv2ex
  388. fveqres
  389. csbfv12
  390. csbfv2g
  391. csbfv
  392. funbrfv
  393. funopfv
  394. fnbrfvb
  395. fnopfvb
  396. funbrfvb
  397. funopfvb
  398. fnbrfvb2
  399. funbrfv2b
  400. dffn5
  401. fnrnfv
  402. fvelrnb
  403. foelrni
  404. dfimafn
  405. dfimafn2
  406. funimass4
  407. fvelima
  408. fvelimad
  409. feqmptd
  410. feqresmpt
  411. feqmptdf
  412. dffn5f
  413. fvelimab
  414. fvelimabd
  415. unima
  416. fvi
  417. fviss
  418. fniinfv
  419. fnsnfv
  420. fnsnfvOLD
  421. opabiotafun
  422. opabiotadm
  423. opabiota
  424. fnimapr
  425. ssimaex
  426. ssimaexg
  427. funfv
  428. funfv2
  429. funfv2f
  430. fvun
  431. fvun1
  432. fvun2
  433. fvun1d
  434. fvun2d
  435. dffv2
  436. dmfco
  437. fvco2
  438. fvco
  439. fvco3
  440. fvco3d
  441. fvco4i
  442. fvopab3g
  443. fvopab3ig
  444. brfvopabrbr
  445. fvmptg
  446. fvmpti
  447. fvmpt
  448. fvmpt2f
  449. fvtresfn
  450. fvmpts
  451. fvmpt3
  452. fvmpt3i
  453. fvmptdf
  454. fvmptd
  455. fvmptd2
  456. mptrcl
  457. fvmpt2i
  458. fvmpt2
  459. fvmptss
  460. fvmpt2d
  461. fvmptex
  462. fvmptd3f
  463. fvmptd2f
  464. fvmptdv
  465. fvmptdv2
  466. mpteqb
  467. fvmptt
  468. fvmptf
  469. fvmptnf
  470. fvmptd3
  471. fvmptn
  472. fvmptss2
  473. elfvmptrab1w
  474. elfvmptrab1
  475. elfvmptrab
  476. fvopab4ndm
  477. fvmptndm
  478. fvmptrabfv
  479. fvopab5
  480. fvopab6
  481. eqfnfv
  482. eqfnfv2
  483. eqfnfv3
  484. eqfnfvd
  485. eqfnfv2f
  486. eqfunfv
  487. fvreseq0
  488. fvreseq1
  489. fvreseq
  490. fnmptfvd
  491. fndmdif
  492. fndmdifcom
  493. fndmdifeq0
  494. fndmin
  495. fneqeql
  496. fneqeql2
  497. fnreseql
  498. chfnrn
  499. funfvop
  500. funfvbrb
  501. fvimacnvi
  502. fvimacnv
  503. funimass3
  504. funimass5
  505. funconstss
  506. fvimacnvALT
  507. elpreima
  508. elpreimad
  509. fniniseg
  510. fncnvima2
  511. fniniseg2
  512. unpreima
  513. inpreima
  514. difpreima
  515. respreima
  516. cnvimainrn
  517. sspreima
  518. iinpreima
  519. intpreima
  520. fimacnvOLD
  521. fimacnvinrn
  522. fimacnvinrn2
  523. rescnvimafod
  524. fvn0ssdmfun
  525. fnopfv
  526. fvelrn
  527. nelrnfvne
  528. fveqdmss
  529. fveqressseq
  530. fnfvelrn
  531. ffvelrn
  532. ffvelrni
  533. ffvelrnda
  534. ffvelrnd
  535. rexrn
  536. ralrn
  537. elrnrexdm
  538. elrnrexdmb
  539. eldmrexrn
  540. eldmrexrnb
  541. fvcofneq
  542. ralrnmptw
  543. rexrnmptw
  544. ralrnmpt
  545. rexrnmpt
  546. f0cli
  547. dff2
  548. dff3
  549. dff4
  550. dffo3
  551. dffo4
  552. dffo5
  553. exfo
  554. foelrn
  555. foco2
  556. fmpt
  557. f1ompt
  558. fmpti
  559. fvmptelrn
  560. fmptd
  561. fmpttd
  562. fmpt3d
  563. fmptdf
  564. ffnfv
  565. ffnfvf
  566. fnfvrnss
  567. frnssb
  568. rnmptss
  569. fmpt2d
  570. ffvresb
  571. f1oresrab
  572. f1ossf1o
  573. fmptco
  574. fmptcof
  575. fmptcos
  576. cofmpt
  577. fcompt
  578. fcoconst
  579. fsn
  580. fsn2
  581. fsng
  582. fsn2g
  583. xpsng
  584. xpprsng
  585. xpsn
  586. f1o2sn
  587. residpr
  588. dfmpt
  589. fnasrn
  590. idref
  591. funiun
  592. funopsn
  593. funop
  594. funopdmsn
  595. funsndifnop
  596. funsneqopb
  597. ressnop0
  598. fpr
  599. fprg
  600. ftpg
  601. ftp
  602. fnressn
  603. funressn
  604. fressnfv
  605. fvrnressn
  606. fvressn
  607. fvn0fvelrn
  608. fvconst
  609. fnsnr
  610. fnsnb
  611. fmptsn
  612. fmptsng
  613. fmptsnd
  614. fmptap
  615. fmptapd
  616. fmptpr
  617. fvresi
  618. fninfp
  619. fnelfp
  620. fndifnfp
  621. fnelnfp
  622. fnnfpeq0
  623. fvunsn
  624. fvsng
  625. fvsn
  626. fvsnun1
  627. fvsnun2
  628. fnsnsplit
  629. fsnunf
  630. fsnunf2
  631. fsnunfv
  632. fsnunres
  633. funresdfunsn
  634. fvpr1g
  635. fvpr2g
  636. fvpr2gOLD
  637. fvpr1
  638. fvpr1OLD
  639. fvpr2
  640. fvpr2OLD
  641. fprb
  642. fvtp1
  643. fvtp2
  644. fvtp3
  645. fvtp1g
  646. fvtp2g
  647. fvtp3g
  648. tpres
  649. fvconst2g
  650. fconst2g
  651. fvconst2
  652. fconst2
  653. fconst5
  654. rnmptc
  655. rnmptcOLD
  656. fnprb
  657. fntpb
  658. fnpr2g
  659. fpr2g
  660. fconstfv
  661. fconst3
  662. fconst4
  663. resfunexg
  664. resiexd
  665. fnex
  666. fnexd
  667. funex
  668. opabex
  669. mptexg
  670. mptexgf
  671. mptex
  672. mptexd
  673. mptrabex
  674. fex
  675. fexd
  676. mptfvmpt
  677. eufnfv
  678. funfvima
  679. funfvima2
  680. funfvima2d
  681. fnfvima
  682. fnfvimad
  683. resfvresima
  684. funfvima3
  685. rexima
  686. ralima
  687. fvclss
  688. elabrex
  689. abrexco
  690. imaiun
  691. imauni
  692. fniunfv
  693. funiunfv
  694. funiunfvf
  695. eluniima
  696. elunirn
  697. elunirnALT
  698. elunirn2
  699. fnunirn
  700. dff13
  701. dff13f
  702. f1veqaeq
  703. f1cofveqaeq
  704. f1cofveqaeqALT
  705. 2f1fvneq
  706. f1mpt
  707. f1fveq
  708. f1elima
  709. f1imass
  710. f1imaeq
  711. f1imapss
  712. fpropnf1
  713. f1dom3fv3dif
  714. f1dom3el3dif
  715. dff14a
  716. dff14b
  717. f12dfv
  718. f13dfv
  719. dff1o6
  720. f1ocnvfv1
  721. f1ocnvfv2
  722. f1ocnvfv
  723. f1ocnvfvb
  724. nvof1o
  725. nvocnv
  726. fsnex
  727. f1prex
  728. f1ocnvdm
  729. f1ocnvfvrneq
  730. fcof1
  731. fcofo
  732. cbvfo
  733. cbvexfo
  734. cocan1
  735. cocan2
  736. fcof1oinvd
  737. fcof1od
  738. 2fcoidinvd
  739. fcof1o
  740. 2fvcoidd
  741. 2fvidf1od
  742. 2fvidinvd
  743. foeqcnvco
  744. f1eqcocnv
  745. f1eqcocnvOLD
  746. fveqf1o
  747. nf1const
  748. nf1oconst
  749. f1ofvswap
  750. fliftrel
  751. fliftel
  752. fliftel1
  753. fliftcnv
  754. fliftfun
  755. fliftfund
  756. fliftfuns
  757. fliftf
  758. fliftval
  759. isoeq1
  760. isoeq2
  761. isoeq3
  762. isoeq4
  763. isoeq5
  764. nfiso
  765. isof1o
  766. isof1oidb
  767. isof1oopb
  768. isorel
  769. soisores
  770. soisoi
  771. isoid
  772. isocnv
  773. isocnv2
  774. isocnv3
  775. isores2
  776. isores1
  777. isores3
  778. isotr
  779. isomin
  780. isoini
  781. isoini2
  782. isofrlem
  783. isoselem
  784. isofr
  785. isose
  786. isofr2
  787. isopolem
  788. isopo
  789. isosolem
  790. isoso
  791. isowe
  792. isowe2
  793. f1oiso
  794. f1oiso2
  795. f1owe
  796. weniso
  797. weisoeq
  798. weisoeq2
  799. knatar