funmpt2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > funmpt2		Structured version Visualization version GIF version

Theorem funmpt2 6363

Description: Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.)

**Hypothesis**
Ref	Expression
funmpt2.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

**Assertion**
Ref	Expression
funmpt2	⊢ Fun 𝐹

**Proof of Theorem funmpt2**
Step	Hyp	Ref	Expression
1		funmpt 6362	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		funmpt2.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	funeqi 6345	. 2 ⊢ (Fun 𝐹 ↔ Fun (𝑥 ∈ 𝐴 ↦ 𝐵))
4	1, 3	mpbir 234	1 ⊢ Fun 𝐹

Colors of variables: wff setvar class

Syntax hints: = wceq 1538 ↦ cmpt 5110 Fun wfun 6318

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-fun 6326

This theorem is referenced by: cantnfp1lem1 9125 tz9.12lem2 9201 tz9.12lem3 9202 rankf 9207 djuun 9339 cardf2 9356 fin23lem30 9753 hashf1rn 13709 funtopon 21525 qustgpopn 22725 ustn0 22826 metuval 23156 cphsscph 23855 ipasslem8 28620 xppreima2 30413 funcnvmpt 30430 fsuppcurry1 30487 fsuppcurry2 30488 gsummpt2co 30733 zarclsint 31225 zartopn 31228 zarmxt1 31233 zarcmplem 31234 metidval 31243 pstmval 31248 brsiga 31552 measbasedom 31571 sseqval 31756 ballotlem7 31903 sinccvglem 33028 bj-evalfun 34488 bj-ccinftydisj 34628 bj-elccinfty 34629 bj-minftyccb 34640 iscard4 40241 harval3 40244 comptiunov2i 40407 icccncfext 42529 stoweidlem27 42669 stirlinglem14 42729 fourierdlem70 42818 fourierdlem71 42819 hoi2toco 43246 mptcfsupp 44782 lcoc0 44831 lincresunit2 44887