Theorem fmpti 7093

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∀wral 3076   ↦ cmpt 5181  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-fun 6523  df-fn 6524  df-f 6525

This theorem is referenced by:  harf  9506  r0weon  9968  dfac2a  10086  ackbij1lem10  10184  cff  10204  isf32lem9  10318  fin1a2lem2  10358  fin1a2lem4  10360  facmapnn  14298  wwlktovf  14969  cjf  15131  ref  15139  imf  15140  absf  15365  limsupcl  15500  limsupgf  15502  eff  16111  sinf  16156  cosf  16157  bitsf  16461  fnum  16777  fden  16778  prmgapprmo  17098  setcepi  18121  catcfuccl  18151  smndex1ibas  18934  smndex2dbas  18951  smndex2hbas  18953  staffval  20887  ocvfval  21715  pjfval  21755  pjpm  21757  psdmul  22228  psdmvr  22231  leordtval2  23269  lecldbas  23276  nmfval  24645  nmoffn  24768  nmofval  24771  divcn  24927  xrhmeo  25005  tcphex  25276  tchnmfval  25287  ioorf  25632  dveflem  26038  tdeglem1  26115  resinf1o  26598  efifo  26609  logcnlem5  26708  resqrtcn  26811  asinf  26934  acosf  26936  atanf  26942  leibpilem2  27003  areaf  27023  emcllem1  27057  igamf  27112  chtf  27169  chpf  27184  ppif  27191  muf  27201  bposlem7  27351  2lgslem1b  27453  pntrf  27624  pntrsumo1  27626  pntsf  27634  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  oldf  27927  newf  27928  leftf  27945  rightf  27946  normf  31323  hosubcli  31969  cnlnadjlem4  32270  cnlnadjlem6  32272  zringfrac  33747  eulerpartlemsf  34653  fiblem  34692  signsvvf  34870  derangf  35515  snmlff  35676  ex-sategoelel12  35774  sinccvglem  36019  circum  36021  dnif  36909  bj-evalf  37561  f1omptsnlem  37827  phpreu  38100  poimirlem26  38142  cncfres  38261  lsatset  39611  clsk1independent  44619  lhe4.4ex1a  44902  absfico  45791  clim1fr1  46174  liminfgf  46329  limsup10ex  46344  liminf10ex  46345  dvsinax  46484  wallispilem5  46640  wallispi  46641  stirlinglem5  46649  stirlinglem13  46657  stirlinglem14  46658  stirlinglem15  46659  stirlingr  46661  fourierdlem43  46721  fourierdlem57  46734  fourierdlem58  46735  fourierdlem62  46739  fouriersw  46802  0ome  47100  sprsymrelf  48098  fmtnof1  48141  prmdvdsfmtnof  48192  uspgrsprf  48765  ackendofnn0  49303