Theorem funmpt2 6575

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

Syntax hints:   = wceq 1568   ↦ cmpt 5191  Fun wfun 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-fun 6538

This theorem is referenced by:  funcnvmpt  6991  pwfilem  9276  cantnfp1lem1  9646  tz9.12lem2  9759  tz9.12lem3  9760  rankf  9765  djuun  9911  cardf2  9928  fin23lem30  10325  hashf1rn  14388  sgnfo  15136  oppccatf  17783  funtopon  23056  qustgpopn  24256  ustn0  24357  cphsscph  25389  ipasslem8  31155  xppreima2  32962  mptiffisupp  33004  fsuppcurry1  33035  fsuppcurry2  33036  gsummpt2co  33334  zarclsint  34228  zartopn  34231  zarmxt1  34236  zarcmplem  34237  brsiga  34539  sseqval  34744  ballotlem7  34892  sinccvglem  36130  bj-evalfun  37680  bj-ccinftydisj  37823  bj-elccinfty  37824  bj-minftyccb  37835  iscard4  44229  harval3  44234  comptiunov2i  44402  icccncfext  46571  stoweidlem27  46711  stirlinglem14  46771  fourierdlem70  46860  fourierdlem71  46861  hoi2toco  47291  mptcfsupp  49124  lcoc0  49169  lincresunit2  49225