Theorem funmpt2 6538

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 6537	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		funmpt2.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	funeqi 6520	. 2 ⊢ (Fun 𝐹 ↔ Fun (𝑥 ∈ 𝐴 ↦ 𝐵))
4	1, 3	mpbir 231	1 ⊢ Fun 𝐹

Syntax hints:   = wceq 1542   ↦ cmpt 5167  Fun wfun 6493

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6501

This theorem is referenced by:  funcnvmpt  6950  pwfilem  9228  cantnfp1lem1  9599  tz9.12lem2  9712  tz9.12lem3  9713  rankf  9718  djuun  9850  cardf2  9867  fin23lem30  10264  hashf1rn  14314  oppccatf  17694  funtopon  22885  qustgpopn  24085  ustn0  24186  cphsscph  25218  ipasslem8  30908  xppreima2  32724  mptiffisupp  32766  fsuppcurry1  32797  fsuppcurry2  32798  gsummpt2co  33109  zarclsint  34016  zartopn  34019  zarmxt1  34024  zarcmplem  34025  brsiga  34327  sseqval  34532  ballotlem7  34680  sinccvglem  35854  bj-evalfun  37384  bj-ccinftydisj  37527  bj-elccinfty  37528  bj-minftyccb  37539  iscard4  43960  harval3  43965  comptiunov2i  44133  icccncfext  46315  stoweidlem27  46455  stirlinglem14  46515  fourierdlem70  46604  fourierdlem71  46605  hoi2toco  47035  mptcfsupp  48847  lcoc0  48892  lincresunit2  48948