Theorem fmpti 6929

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  ∀wral 3061   ↦ cmpt 5135  ⟶wf 6376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-fun 6382  df-fn 6383  df-f 6384

This theorem is referenced by:  harf  9174  r0weon  9626  dfac2a  9743  ackbij1lem10  9843  cff  9862  isf32lem9  9975  fin1a2lem2  10015  fin1a2lem4  10017  facmapnn  13851  wwlktovf  14523  cjf  14667  ref  14675  imf  14676  absf  14901  limsupcl  15034  limsupgf  15036  eff  15643  sinf  15685  cosf  15686  bitsf  15986  fnum  16298  fden  16299  prmgapprmo  16615  setcepi  17594  catcfuccl  17625  catcfucclOLD  17626  smndex1ibas  18327  smndex2dbas  18341  smndex2hbas  18343  staffval  19883  ocvfval  20628  pjfval  20668  pjpm  20670  leordtval2  22109  lecldbas  22116  nmfval  23486  nmoffn  23609  nmofval  23612  divcn  23765  xrhmeo  23843  tcphex  24114  tchnmfval  24125  ioorf  24470  dveflem  24876  tdeglem1  24953  resinf1o  25425  efifo  25436  logcnlem5  25534  resqrtcn  25635  asinf  25755  acosf  25757  atanf  25763  leibpilem2  25824  areaf  25844  emcllem1  25878  igamf  25933  chtf  25990  chpf  26005  ppif  26012  muf  26022  bposlem7  26171  2lgslem1b  26273  pntrf  26444  pntrsumo1  26446  pntsf  26454  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  normf  29204  hosubcli  29850  cnlnadjlem4  30151  cnlnadjlem6  30153  eulerpartlemsf  32038  fiblem  32077  signsvvf  32270  derangf  32843  snmlff  33004  ex-sategoelel12  33102  sinccvglem  33343  circum  33345  oldf  33778  newf  33779  leftf  33786  rightf  33787  dnif  34391  f1omptsnlem  35244  phpreu  35498  poimirlem26  35540  cncfres  35660  lsatset  36741  clsk1independent  41333  lhe4.4ex1a  41620  absfico  42431  clim1fr1  42817  liminfgf  42974  limsup10ex  42989  liminf10ex  42990  dvsinax  43129  wallispilem5  43285  wallispi  43286  stirlinglem5  43294  stirlinglem13  43302  stirlinglem14  43303  stirlinglem15  43304  stirlingr  43306  fourierdlem43  43366  fourierdlem57  43379  fourierdlem58  43380  fourierdlem62  43384  fouriersw  43447  0ome  43742  sprsymrelf  44620  fmtnof1  44660  prmdvdsfmtnof  44711  uspgrsprf  44981  ackendofnn0  45703