Metamath Proof Explorer


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