Theorem fmpti 7107

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079   ↦ cmpt 5192  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  harf  9516  r0weon  9992  dfac2a  10109  ackbij1lem10  10207  cff  10226  isf32lem9  10340  fin1a2lem2  10380  fin1a2lem4  10382  facmapnn  14317  wwlktovf  14989  cjf  15151  ref  15159  imf  15160  absf  15385  limsupcl  15520  limsupgf  15522  eff  16130  sinf  16175  cosf  16176  bitsf  16480  fnum  16796  fden  16797  prmgapprmo  17117  setcepi  18140  catcfuccl  18170  smndex1ibas  18954  smndex2dbas  18971  smndex2hbas  18973  staffval  20944  ocvfval  21816  pjfval  21856  pjpm  21858  psdmul  22329  psdmvr  22332  leordtval2  23369  lecldbas  23376  nmfval  24745  nmoffn  24868  nmofval  24871  divcn  25027  xrhmeo  25105  tcphex  25376  tchnmfval  25387  ioorf  25732  dveflem  26138  tdeglem1  26215  resinf1o  26701  efifo  26712  logcnlem5  26811  resqrtcn  26914  asinf  27037  acosf  27039  atanf  27045  leibpilem2  27106  areaf  27126  emcllem1  27160  igamf  27215  chtf  27272  chpf  27287  ppif  27294  muf  27304  bposlem7  27454  2lgslem1b  27556  pntrf  27727  pntrsumo1  27729  pntsf  27737  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  oldf  28030  newf  28031  leftf  28048  rightf  28049  normf  31475  hosubcli  32121  cnlnadjlem4  32422  cnlnadjlem6  32424  zringfrac  33844  eulerpartlemsf  34749  fiblem  34788  signsvvf  34966  derangf  35660  snmlff  35821  ex-sategoelel12  35919  sinccvglem  36164  circum  36166  dnif  37063  bj-evalf  37716  f1omptsnlem  37982  phpreu  38255  poimirlem26  38297  cncfres  38416  lsatset  39764  clsk1independent  44772  lhe4.4ex1a  45039  absfico  45934  clim1fr1  46317  liminfgf  46472  limsup10ex  46487  liminf10ex  46488  dvsinax  46627  wallispilem5  46783  wallispi  46784  stirlinglem5  46792  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  stirlingr  46804  fourierdlem43  46864  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fouriersw  46945  0ome  47243  sprsymrelf  48244  fmtnof1  48287  prmdvdsfmtnof  48338  uspgrsprf  48911  ackendofnn0  49464