Theorem fmpti 6705

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

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  ∀wral 3090   ↦ cmpt 5013  ⟶wf 6189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-sep 5064  ax-nul 5071  ax-pr 5190

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3419  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-fv 6201

This theorem is referenced by:  harf  8825  r0weon  9238  dfac2a  9355  ackbij1lem10  9455  cff  9474  isf32lem9  9587  fin1a2lem2  9627  fin1a2lem4  9629  facmapnn  13466  wwlktovf  14187  cjf  14330  ref  14338  imf  14339  absf  14564  limsupcl  14697  limsupgf  14699  eff  15301  sinf  15343  cosf  15344  bitsf  15642  fnum  15944  fden  15945  prmgapprmo  16260  setcepi  17218  catcfuccl  17239  staffval  19352  ocvfval  20527  pjfval  20567  pjpm  20569  leordtval2  21539  lecldbas  21546  nmfval  22916  nmoffn  23038  nmofval  23041  divcn  23194  xrhmeo  23268  tcphex  23538  tchnmfval  23549  ioorf  23892  dveflem  24294  resinf1o  24836  efifo  24847  logcnlem5  24945  resqrtcn  25046  asinf  25166  acosf  25168  atanf  25174  leibpilem2  25236  areaf  25256  emcllem1  25290  igamf  25345  chtf  25402  chpf  25417  ppif  25424  muf  25434  bposlem7  25583  2lgslem1b  25685  pntrf  25856  pntrsumo1  25858  pntsf  25866  pntrlog2bndlem4  25873  pntrlog2bndlem5  25874  normf  28694  hosubcli  29342  cnlnadjlem4  29643  cnlnadjlem6  29645  eulerpartlemsf  31294  fiblem  31334  signsvvf  31529  derangf  32040  snmlff  32201  sinccvglem  32475  circum  32477  dnif  33373  f1omptsnlem  34099  phpreu  34357  poimirlem26  34399  cncfres  34525  lsatset  35611  clsk1independent  39800  lhe4.4ex1a  40118  absfico  40942  clim1fr1  41348  liminfgf  41505  limsup10ex  41520  liminf10ex  41521  dvsinax  41662  wallispilem5  41820  wallispi  41821  stirlinglem5  41829  stirlinglem13  41837  stirlinglem14  41838  stirlinglem15  41839  stirlingr  41841  fourierdlem43  41901  fourierdlem57  41914  fourierdlem58  41915  fourierdlem62  41919  fouriersw  41982  0ome  42277  sprsymrelf  43060  fmtnof1  43100  prmdvdsfmtnof  43151  uspgrsprf  43424