Theorem funmpt2 6558

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

Syntax hints:   = wceq 1540   ↦ cmpt 5191  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  pwfilem  9274  cantnfp1lem1  9638  tz9.12lem2  9748  tz9.12lem3  9749  rankf  9754  djuun  9886  cardf2  9903  fin23lem30  10302  hashf1rn  14324  oppccatf  17696  funtopon  22814  qustgpopn  24014  ustn0  24115  cphsscph  25158  ipasslem8  30773  xppreima2  32582  funcnvmpt  32598  mptiffisupp  32623  fsuppcurry1  32655  fsuppcurry2  32656  gsummpt2co  32995  zarclsint  33869  zartopn  33872  zarmxt1  33877  zarcmplem  33878  brsiga  34180  sseqval  34386  ballotlem7  34534  sinccvglem  35666  bj-evalfun  37068  bj-ccinftydisj  37208  bj-elccinfty  37209  bj-minftyccb  37220  iscard4  43529  harval3  43534  comptiunov2i  43702  icccncfext  45892  stoweidlem27  46032  stirlinglem14  46092  fourierdlem70  46181  fourierdlem71  46182  hoi2toco  46612  mptcfsupp  48369  lcoc0  48415  lincresunit2  48471