Theorem funmpt2 6591

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

Syntax hints:   = wceq 1533   ↦ cmpt 5231  Fun wfun 6541

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 5299  ax-nul 5306  ax-pr 5428

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 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-fun 6549

This theorem is referenced by:  pwfilem  9200  cantnfp1lem1  9701  tz9.12lem2  9811  tz9.12lem3  9812  rankf  9817  djuun  9949  cardf2  9966  fin23lem30  10365  hashf1rn  14343  oppccatf  17709  funtopon  22852  qustgpopn  24054  ustn0  24155  cphsscph  25209  ipasslem8  30703  xppreima2  32494  funcnvmpt  32510  mptiffisupp  32530  fsuppcurry1  32564  fsuppcurry2  32565  gsummpt2co  32819  zarclsint  33543  zartopn  33546  zarmxt1  33551  zarcmplem  33552  brsiga  33872  sseqval  34078  ballotlem7  34225  sinccvglem  35346  bj-evalfun  36622  bj-ccinftydisj  36762  bj-elccinfty  36763  bj-minftyccb  36774  iscard4  43028  harval3  43033  comptiunov2i  43201  icccncfext  45338  stoweidlem27  45478  stirlinglem14  45538  fourierdlem70  45627  fourierdlem71  45628  hoi2toco  46058  mptcfsupp  47556  lcoc0  47602  lincresunit2  47658