Theorem funmpt2 6516

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

Syntax hints:   = wceq 1541   ↦ cmpt 5170  Fun wfun 6471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  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 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-fun 6479

This theorem is referenced by:  pwfilem  9197  cantnfp1lem1  9563  tz9.12lem2  9673  tz9.12lem3  9674  rankf  9679  djuun  9811  cardf2  9828  fin23lem30  10225  hashf1rn  14251  oppccatf  17626  funtopon  22828  qustgpopn  24028  ustn0  24129  cphsscph  25171  ipasslem8  30807  xppreima2  32623  funcnvmpt  32639  mptiffisupp  32664  fsuppcurry1  32697  fsuppcurry2  32698  gsummpt2co  33018  zarclsint  33875  zartopn  33878  zarmxt1  33883  zarcmplem  33884  brsiga  34186  sseqval  34391  ballotlem7  34539  sinccvglem  35684  bj-evalfun  37086  bj-ccinftydisj  37226  bj-elccinfty  37227  bj-minftyccb  37238  iscard4  43545  harval3  43550  comptiunov2i  43718  icccncfext  45904  stoweidlem27  46044  stirlinglem14  46104  fourierdlem70  46193  fourierdlem71  46194  hoi2toco  46624  mptcfsupp  48387  lcoc0  48433  lincresunit2  48489