Theorem funmpt2 6607

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

Syntax hints:   = wceq 1537   ↦ cmpt 5231  Fun wfun 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-fun 6565

This theorem is referenced by:  pwfilem  9354  cantnfp1lem1  9716  tz9.12lem2  9826  tz9.12lem3  9827  rankf  9832  djuun  9964  cardf2  9981  fin23lem30  10380  hashf1rn  14388  oppccatf  17775  funtopon  22942  qustgpopn  24144  ustn0  24245  cphsscph  25299  ipasslem8  30866  xppreima2  32668  funcnvmpt  32684  mptiffisupp  32708  fsuppcurry1  32743  fsuppcurry2  32744  gsummpt2co  33034  zarclsint  33833  zartopn  33836  zarmxt1  33841  zarcmplem  33842  brsiga  34164  sseqval  34370  ballotlem7  34517  sinccvglem  35657  bj-evalfun  37056  bj-ccinftydisj  37196  bj-elccinfty  37197  bj-minftyccb  37208  iscard4  43523  harval3  43528  comptiunov2i  43696  icccncfext  45843  stoweidlem27  45983  stirlinglem14  46043  fourierdlem70  46132  fourierdlem71  46133  hoi2toco  46563  mptcfsupp  48222  lcoc0  48268  lincresunit2  48324