Theorem fmpti 7051

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∀wral 3047   ↦ cmpt 5174  ⟶wf 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6489  df-fn 6490  df-f 6491

This theorem is referenced by:  harf  9450  r0weon  9909  dfac2a  10027  ackbij1lem10  10125  cff  10145  isf32lem9  10258  fin1a2lem2  10298  fin1a2lem4  10300  facmapnn  14198  wwlktovf  14869  cjf  15017  ref  15025  imf  15026  absf  15251  limsupcl  15386  limsupgf  15388  eff  15994  sinf  16039  cosf  16040  bitsf  16344  fnum  16659  fden  16660  prmgapprmo  16980  setcepi  18001  catcfuccl  18031  smndex1ibas  18814  smndex2dbas  18828  smndex2hbas  18830  staffval  20762  ocvfval  21609  pjfval  21649  pjpm  21651  psdmul  22087  psdmvr  22090  leordtval2  23133  lecldbas  23140  nmfval  24509  nmoffn  24632  nmofval  24635  divcnOLD  24790  divcn  24792  xrhmeo  24877  tcphex  25150  tchnmfval  25161  ioorf  25507  dveflem  25916  tdeglem1  25996  resinf1o  26478  efifo  26489  logcnlem5  26588  resqrtcn  26692  asinf  26815  acosf  26817  atanf  26823  leibpilem2  26884  areaf  26904  emcllem1  26939  igamf  26994  chtf  27051  chpf  27066  ppif  27073  muf  27083  bposlem7  27234  2lgslem1b  27336  pntrf  27507  pntrsumo1  27509  pntsf  27517  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  oldf  27804  newf  27805  leftf  27816  rightf  27817  normf  31110  hosubcli  31756  cnlnadjlem4  32057  cnlnadjlem6  32059  zringfrac  33526  eulerpartlemsf  34379  fiblem  34418  signsvvf  34599  derangf  35219  snmlff  35380  ex-sategoelel12  35478  sinccvglem  35723  circum  35725  dnif  36525  f1omptsnlem  37387  phpreu  37650  poimirlem26  37692  cncfres  37811  lsatset  39095  clsk1independent  44144  lhe4.4ex1a  44427  absfico  45320  clim1fr1  45706  liminfgf  45861  limsup10ex  45876  liminf10ex  45877  dvsinax  46016  wallispilem5  46172  wallispi  46173  stirlinglem5  46181  stirlinglem13  46189  stirlinglem14  46190  stirlinglem15  46191  stirlingr  46193  fourierdlem43  46253  fourierdlem57  46266  fourierdlem58  46267  fourierdlem62  46271  fouriersw  46334  0ome  46632  sprsymrelf  47600  fmtnof1  47640  prmdvdsfmtnof  47691  uspgrsprf  48251  ackendofnn0  48790