Theorem fmpti 7053

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3053   ↦ cmpt 5153  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fun 6487  df-fn 6488  df-f 6489

This theorem is referenced by:  harf  9463  r0weon  9925  dfac2a  10043  ackbij1lem10  10141  cff  10161  isf32lem9  10274  fin1a2lem2  10314  fin1a2lem4  10316  facmapnn  14238  wwlktovf  14909  cjf  15057  ref  15065  imf  15066  absf  15291  limsupcl  15426  limsupgf  15428  eff  16037  sinf  16082  cosf  16083  bitsf  16387  fnum  16703  fden  16704  prmgapprmo  17024  setcepi  18046  catcfuccl  18076  smndex1ibas  18859  smndex2dbas  18876  smndex2hbas  18878  staffval  20813  ocvfval  21641  pjfval  21681  pjpm  21683  psdmul  22154  psdmvr  22157  leordtval2  23195  lecldbas  23202  nmfval  24571  nmoffn  24694  nmofval  24697  divcn  24853  xrhmeo  24931  tcphex  25202  tchnmfval  25213  ioorf  25558  dveflem  25964  tdeglem1  26041  resinf1o  26518  efifo  26529  logcnlem5  26628  resqrtcn  26731  asinf  26854  acosf  26856  atanf  26862  leibpilem2  26923  areaf  26943  emcllem1  26977  igamf  27032  chtf  27089  chpf  27104  ppif  27111  muf  27121  bposlem7  27271  2lgslem1b  27373  pntrf  27544  pntrsumo1  27546  pntsf  27554  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  oldf  27847  newf  27848  leftf  27865  rightf  27866  normf  31212  hosubcli  31858  cnlnadjlem4  32159  cnlnadjlem6  32161  zringfrac  33637  eulerpartlemsf  34543  fiblem  34582  signsvvf  34763  derangf  35396  snmlff  35557  ex-sategoelel12  35655  sinccvglem  35900  circum  35902  dnif  36780  bj-evalf  37432  f1omptsnlem  37698  phpreu  37971  poimirlem26  38013  cncfres  38132  lsatset  39482  clsk1independent  44490  lhe4.4ex1a  44773  absfico  45663  clim1fr1  46046  liminfgf  46201  limsup10ex  46216  liminf10ex  46217  dvsinax  46356  wallispilem5  46512  wallispi  46513  stirlinglem5  46521  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  stirlingr  46533  fourierdlem43  46593  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fouriersw  46674  0ome  46972  sprsymrelf  47970  fmtnof1  48013  prmdvdsfmtnof  48064  uspgrsprf  48637  ackendofnn0  49175