Theorem fmpti 7055

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3049   ↦ cmpt 5177  ⟶wf 6486

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  harf  9461  r0weon  9920  dfac2a  10038  ackbij1lem10  10136  cff  10156  isf32lem9  10269  fin1a2lem2  10309  fin1a2lem4  10311  facmapnn  14206  wwlktovf  14877  cjf  15025  ref  15033  imf  15034  absf  15259  limsupcl  15394  limsupgf  15396  eff  16002  sinf  16047  cosf  16048  bitsf  16352  fnum  16667  fden  16668  prmgapprmo  16988  setcepi  18010  catcfuccl  18040  smndex1ibas  18823  smndex2dbas  18837  smndex2hbas  18839  staffval  20772  ocvfval  21619  pjfval  21659  pjpm  21661  psdmul  22107  psdmvr  22110  leordtval2  23154  lecldbas  23161  nmfval  24530  nmoffn  24653  nmofval  24656  divcnOLD  24811  divcn  24813  xrhmeo  24898  tcphex  25171  tchnmfval  25182  ioorf  25528  dveflem  25937  tdeglem1  26017  resinf1o  26499  efifo  26510  logcnlem5  26609  resqrtcn  26713  asinf  26836  acosf  26838  atanf  26844  leibpilem2  26905  areaf  26925  emcllem1  26960  igamf  27015  chtf  27072  chpf  27087  ppif  27094  muf  27104  bposlem7  27255  2lgslem1b  27357  pntrf  27528  pntrsumo1  27530  pntsf  27538  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  oldf  27825  newf  27826  leftf  27837  rightf  27838  normf  31147  hosubcli  31793  cnlnadjlem4  32094  cnlnadjlem6  32096  zringfrac  33584  eulerpartlemsf  34465  fiblem  34504  signsvvf  34685  derangf  35311  snmlff  35472  ex-sategoelel12  35570  sinccvglem  35815  circum  35817  dnif  36617  f1omptsnlem  37480  phpreu  37744  poimirlem26  37786  cncfres  37905  lsatset  39189  clsk1independent  44229  lhe4.4ex1a  44512  absfico  45404  clim1fr1  45789  liminfgf  45944  limsup10ex  45959  liminf10ex  45960  dvsinax  46099  wallispilem5  46255  wallispi  46256  stirlinglem5  46264  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  stirlingr  46276  fourierdlem43  46336  fourierdlem57  46349  fourierdlem58  46350  fourierdlem62  46354  fouriersw  46417  0ome  46715  sprsymrelf  47683  fmtnof1  47723  prmdvdsfmtnof  47774  uspgrsprf  48334  ackendofnn0  48872