Theorem funmpt2 6470

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

Syntax hints:   = wceq 1542   ↦ cmpt 5162  Fun wfun 6425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-fun 6433

This theorem is referenced by:  pwfilem  8940  cantnfp1lem1  9412  tz9.12lem2  9545  tz9.12lem3  9546  rankf  9551  djuun  9683  cardf2  9700  fin23lem30  10097  hashf1rn  14063  oppccatf  17435  funtopon  22065  qustgpopn  23267  ustn0  23368  metuval  23701  cphsscph  24411  ipasslem8  29193  xppreima2  30982  funcnvmpt  30998  fsuppcurry1  31054  fsuppcurry2  31055  gsummpt2co  31302  zarclsint  31816  zartopn  31819  zarmxt1  31824  zarcmplem  31825  metidval  31834  pstmval  31839  brsiga  32145  measbasedom  32164  sseqval  32349  ballotlem7  32496  sinccvglem  33624  bj-evalfun  35238  bj-ccinftydisj  35378  bj-elccinfty  35379  bj-minftyccb  35390  iscard4  41117  harval3  41120  comptiunov2i  41282  icccncfext  43397  stoweidlem27  43537  stirlinglem14  43597  fourierdlem70  43686  fourierdlem71  43687  hoi2toco  44114  mptcfsupp  45683  lcoc0  45730  lincresunit2  45786