Theorem funmpt2 6539

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

Syntax hints:   = wceq 1542   ↦ cmpt 5181  Fun wfun 6494

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-fun 6502

This theorem is referenced by:  funcnvmpt  6951  pwfilem  9230  cantnfp1lem1  9599  tz9.12lem2  9712  tz9.12lem3  9713  rankf  9718  djuun  9850  cardf2  9867  fin23lem30  10264  hashf1rn  14287  oppccatf  17663  funtopon  22876  qustgpopn  24076  ustn0  24177  cphsscph  25219  ipasslem8  30924  xppreima2  32740  mptiffisupp  32782  fsuppcurry1  32813  fsuppcurry2  32814  gsummpt2co  33141  zarclsint  34049  zartopn  34052  zarmxt1  34057  zarcmplem  34058  brsiga  34360  sseqval  34565  ballotlem7  34713  sinccvglem  35885  bj-evalfun  37316  bj-ccinftydisj  37457  bj-elccinfty  37458  bj-minftyccb  37469  iscard4  43878  harval3  43883  comptiunov2i  44051  icccncfext  46234  stoweidlem27  46374  stirlinglem14  46434  fourierdlem70  46523  fourierdlem71  46524  hoi2toco  46954  mptcfsupp  48726  lcoc0  48771  lincresunit2  48827