Theorem fmpti 6869

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 3147	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵
3		fmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
4	3	fmpt 6867	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
5	2, 4	mpbi 232	1 ⊢ 𝐹:𝐴⟶𝐵

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  ∀wral 3137   ↦ cmpt 5139  ⟶wf 6344

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pr 5323

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3493  df-sbc 3769  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356

This theorem is referenced by:  harf  9017  r0weon  9431  dfac2a  9548  ackbij1lem10  9644  cff  9663  isf32lem9  9776  fin1a2lem2  9816  fin1a2lem4  9818  facmapnn  13642  wwlktovf  14315  cjf  14458  ref  14466  imf  14467  absf  14692  limsupcl  14825  limsupgf  14827  eff  15430  sinf  15472  cosf  15473  bitsf  15771  fnum  16077  fden  16078  prmgapprmo  16393  setcepi  17343  catcfuccl  17364  smndex1ibas  18060  smndex2dbas  18074  smndex2hbas  18076  staffval  19613  ocvfval  20805  pjfval  20845  pjpm  20847  leordtval2  21815  lecldbas  21822  nmfval  23193  nmoffn  23315  nmofval  23318  divcn  23471  xrhmeo  23545  tcphex  23815  tchnmfval  23826  ioorf  24169  dveflem  24573  resinf1o  25118  efifo  25129  logcnlem5  25227  resqrtcn  25328  asinf  25448  acosf  25450  atanf  25456  leibpilem2  25517  areaf  25537  emcllem1  25571  igamf  25626  chtf  25683  chpf  25698  ppif  25705  muf  25715  bposlem7  25864  2lgslem1b  25966  pntrf  26137  pntrsumo1  26139  pntsf  26147  pntrlog2bndlem4  26154  pntrlog2bndlem5  26155  normf  28898  hosubcli  29544  cnlnadjlem4  29845  cnlnadjlem6  29847  eulerpartlemsf  31638  fiblem  31677  signsvvf  31870  derangf  32436  snmlff  32597  ex-sategoelel12  32695  sinccvglem  32936  circum  32938  dnif  33834  f1omptsnlem  34641  phpreu  34911  poimirlem26  34953  cncfres  35076  lsatset  36159  clsk1independent  40470  lhe4.4ex1a  40735  absfico  41555  clim1fr1  41956  liminfgf  42113  limsup10ex  42128  liminf10ex  42129  dvsinax  42271  wallispilem5  42428  wallispi  42429  stirlinglem5  42437  stirlinglem13  42445  stirlinglem14  42446  stirlinglem15  42447  stirlingr  42449  fourierdlem43  42509  fourierdlem57  42522  fourierdlem58  42523  fourierdlem62  42527  fouriersw  42590  0ome  42885  sprsymrelf  43731  fmtnof1  43771  prmdvdsfmtnof  43822  uspgrsprf  44095