Theorem fmpti 6980

Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)

Hypotheses

Ref	Expression
fmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
fmpti.2	⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Assertion

Ref	Expression
fmpti	⊢ 𝐹:𝐴⟶𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem fmpti

Step	Hyp	Ref	Expression
1		fmpti.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
2	1	rgen 3075	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
3		fmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
4	3	fmpt 6978	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
5	2, 4	mpbi 229	1 ⊢ 𝐹:𝐴⟶𝐵

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  ∀wral 3065   ↦ cmpt 5161  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-fun 6432  df-fn 6433  df-f 6434

This theorem is referenced by:  harf  9278  r0weon  9752  dfac2a  9869  ackbij1lem10  9969  cff  9988  isf32lem9  10101  fin1a2lem2  10141  fin1a2lem4  10143  facmapnn  13980  wwlktovf  14652  cjf  14796  ref  14804  imf  14805  absf  15030  limsupcl  15163  limsupgf  15165  eff  15772  sinf  15814  cosf  15815  bitsf  16115  fnum  16427  fden  16428  prmgapprmo  16744  setcepi  17784  catcfuccl  17815  catcfucclOLD  17816  smndex1ibas  18520  smndex2dbas  18534  smndex2hbas  18536  staffval  20088  ocvfval  20852  pjfval  20894  pjpm  20896  leordtval2  22344  lecldbas  22351  nmfval  23725  nmoffn  23856  nmofval  23859  divcn  24012  xrhmeo  24090  tcphex  24362  tchnmfval  24373  ioorf  24718  dveflem  25124  tdeglem1  25201  resinf1o  25673  efifo  25684  logcnlem5  25782  resqrtcn  25883  asinf  26003  acosf  26005  atanf  26011  leibpilem2  26072  areaf  26092  emcllem1  26126  igamf  26181  chtf  26238  chpf  26253  ppif  26260  muf  26270  bposlem7  26419  2lgslem1b  26521  pntrf  26692  pntrsumo1  26694  pntsf  26702  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  normf  29464  hosubcli  30110  cnlnadjlem4  30411  cnlnadjlem6  30413  eulerpartlemsf  32305  fiblem  32344  signsvvf  32537  derangf  33109  snmlff  33270  ex-sategoelel12  33368  sinccvglem  33609  circum  33611  oldf  34020  newf  34021  leftf  34028  rightf  34029  dnif  34633  f1omptsnlem  35486  phpreu  35740  poimirlem26  35782  cncfres  35902  lsatset  36983  clsk1independent  41609  lhe4.4ex1a  41900  absfico  42711  clim1fr1  43096  liminfgf  43253  limsup10ex  43268  liminf10ex  43269  dvsinax  43408  wallispilem5  43564  wallispi  43565  stirlinglem5  43573  stirlinglem13  43581  stirlinglem14  43582  stirlinglem15  43583  stirlingr  43585  fourierdlem43  43645  fourierdlem57  43658  fourierdlem58  43659  fourierdlem62  43663  fouriersw  43726  0ome  44021  sprsymrelf  44899  fmtnof1  44939  prmdvdsfmtnof  44990  uspgrsprf  45260  ackendofnn0  45982