Theorem funmpt2 6532

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

Syntax hints:   = wceq 1542   ↦ cmpt 5180  Fun wfun 6487

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6495

This theorem is referenced by:  funcnvmpt  6944  pwfilem  9222  cantnfp1lem1  9591  tz9.12lem2  9704  tz9.12lem3  9705  rankf  9710  djuun  9842  cardf2  9859  fin23lem30  10256  hashf1rn  14279  oppccatf  17655  funtopon  22868  qustgpopn  24068  ustn0  24169  cphsscph  25211  ipasslem8  30895  xppreima2  32711  mptiffisupp  32753  fsuppcurry1  32784  fsuppcurry2  32785  gsummpt2co  33112  zarclsint  34010  zartopn  34013  zarmxt1  34018  zarcmplem  34019  brsiga  34321  sseqval  34526  ballotlem7  34674  sinccvglem  35847  bj-evalfun  37249  bj-ccinftydisj  37389  bj-elccinfty  37390  bj-minftyccb  37401  iscard4  43810  harval3  43815  comptiunov2i  43983  icccncfext  46167  stoweidlem27  46307  stirlinglem14  46367  fourierdlem70  46456  fourierdlem71  46457  hoi2toco  46887  mptcfsupp  48659  lcoc0  48704  lincresunit2  48760