Theorem funmpt2 6525

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

Syntax hints:   = wceq 1540   ↦ cmpt 5176  Fun wfun 6480

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-fun 6488

This theorem is referenced by:  pwfilem  9225  cantnfp1lem1  9593  tz9.12lem2  9703  tz9.12lem3  9704  rankf  9709  djuun  9841  cardf2  9858  fin23lem30  10255  hashf1rn  14277  oppccatf  17652  funtopon  22823  qustgpopn  24023  ustn0  24124  cphsscph  25167  ipasslem8  30799  xppreima2  32608  funcnvmpt  32624  mptiffisupp  32649  fsuppcurry1  32681  fsuppcurry2  32682  gsummpt2co  33014  zarclsint  33838  zartopn  33841  zarmxt1  33846  zarcmplem  33847  brsiga  34149  sseqval  34355  ballotlem7  34503  sinccvglem  35644  bj-evalfun  37046  bj-ccinftydisj  37186  bj-elccinfty  37187  bj-minftyccb  37198  iscard4  43506  harval3  43511  comptiunov2i  43679  icccncfext  45869  stoweidlem27  46009  stirlinglem14  46069  fourierdlem70  46158  fourierdlem71  46159  hoi2toco  46589  mptcfsupp  48349  lcoc0  48395  lincresunit2  48451