Theorem funmpt2 6593

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

Syntax hints:   = wceq 1533   ↦ cmpt 5232  Fun wfun 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-fun 6551

This theorem is referenced by:  pwfilem  9202  cantnfp1lem1  9703  tz9.12lem2  9813  tz9.12lem3  9814  rankf  9819  djuun  9951  cardf2  9968  fin23lem30  10367  hashf1rn  14347  oppccatf  17713  funtopon  22866  qustgpopn  24068  ustn0  24169  cphsscph  25223  ipasslem8  30719  xppreima2  32518  funcnvmpt  32534  mptiffisupp  32555  fsuppcurry1  32589  fsuppcurry2  32590  gsummpt2co  32852  zarclsint  33604  zartopn  33607  zarmxt1  33612  zarcmplem  33613  brsiga  33933  sseqval  34139  ballotlem7  34286  sinccvglem  35407  bj-evalfun  36683  bj-ccinftydisj  36823  bj-elccinfty  36824  bj-minftyccb  36835  iscard4  43105  harval3  43110  comptiunov2i  43278  icccncfext  45413  stoweidlem27  45553  stirlinglem14  45613  fourierdlem70  45702  fourierdlem71  45703  hoi2toco  46133  mptcfsupp  47630  lcoc0  47676  lincresunit2  47732