Theorem funmpt2 6529

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

Syntax hints:   = wceq 1542   ↦ cmpt 5167  Fun wfun 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-fun 6492

This theorem is referenced by:  funcnvmpt  6941  pwfilem  9219  cantnfp1lem1  9588  tz9.12lem2  9701  tz9.12lem3  9702  rankf  9707  djuun  9839  cardf2  9856  fin23lem30  10253  hashf1rn  14303  oppccatf  17683  funtopon  22894  qustgpopn  24094  ustn0  24195  cphsscph  25227  ipasslem8  30928  xppreima2  32744  mptiffisupp  32786  fsuppcurry1  32817  fsuppcurry2  32818  gsummpt2co  33129  zarclsint  34037  zartopn  34040  zarmxt1  34045  zarcmplem  34046  brsiga  34348  sseqval  34553  ballotlem7  34701  sinccvglem  35875  bj-evalfun  37397  bj-ccinftydisj  37540  bj-elccinfty  37541  bj-minftyccb  37552  iscard4  43975  harval3  43980  comptiunov2i  44148  icccncfext  46330  stoweidlem27  46470  stirlinglem14  46530  fourierdlem70  46619  fourierdlem71  46620  hoi2toco  47050  mptcfsupp  48850  lcoc0  48895  lincresunit2  48951