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