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 𝐹

This proof depends on syntax axioms:   = wceq 1569   ↦ cmpt 5191  Fun wfun 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  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 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-fun 6538

This theorem is used by:  funcnvmpt  6991  pwfilem  9275  cantnfp1lem1  9645  tz9.12lem2  9758  tz9.12lem3  9759  rankf  9764  djuun  9919  cardf2  9936  fin23lem30  10332  hashf1rn  14395  sgnfo  15143  oppccatf  17790  funtopon  23088  qustgpopn  24288  ustn0  24389  cphsscph  25421  ipasslem8  31200  xppreima2  33007  mptiffisupp  33049  fsuppcurry1  33080  fsuppcurry2  33081  gsummpt2co  33377  zarclsint  34271  zartopn  34274  zarmxt1  34279  zarcmplem  34280  brsiga  34582  sseqval  34787  ballotlem7  34935  sinccvglem  36172  bj-evalfun  37742  bj-ccinftydisj  37885  bj-elccinfty  37886  bj-minftyccb  37897  iscard4  44287  harval3  44292  comptiunov2i  44460  icccncfext  46629  stoweidlem27  46769  stirlinglem14  46829  fourierdlem70  46918  fourierdlem71  46919  hoi2toco  47349  mptcfsupp  49185  lcoc0  49230  lincresunit2  49286