Theorem fmpti 6546

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  ∀wral 3050   ↦ cmpt 4881  ⟶wf 6045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057

This theorem is referenced by:  harf  8630  r0weon  9025  dfac2a  9142  ackbij1lem10  9243  cff  9262  isf32lem9  9375  fin1a2lem2  9415  fin1a2lem4  9417  facmapnn  13266  wwlktovf  13900  cjf  14043  ref  14051  imf  14052  absf  14276  limsupcl  14403  limsupgf  14405  eff  15011  sinf  15053  cosf  15054  bitsf  15351  fnum  15652  fden  15653  prmgapprmo  15968  setcepi  16939  catcfuccl  16960  staffval  19049  ocvfval  20212  pjfval  20252  pjpm  20254  leordtval2  21218  lecldbas  21225  nmfval  22594  nmoffn  22716  nmofval  22719  divcn  22872  xrhmeo  22946  tchex  23216  tchnmfval  23227  ioorf  23541  dveflem  23941  resinf1o  24481  efifo  24492  logcnlem5  24591  resqrtcn  24689  asinf  24798  acosf  24800  atanf  24806  leibpilem2  24867  areaf  24887  emcllem1  24921  igamf  24976  chtf  25033  chpf  25048  ppif  25055  muf  25065  bposlem7  25214  2lgslem1b  25316  pntrf  25451  pntrsumo1  25453  pntsf  25461  pntrlog2bndlem4  25468  pntrlog2bndlem5  25469  normf  28289  hosubcli  28937  cnlnadjlem4  29238  cnlnadjlem6  29240  eulerpartlemsf  30730  fiblem  30769  signsvvf  30965  derangf  31457  snmlff  31618  sinccvglem  31873  circum  31875  dnif  32770  f1omptsnlem  33494  phpreu  33706  poimirlem26  33748  cncfres  33877  lsatset  34780  clsk1independent  38846  lhe4.4ex1a  39030  absfico  39909  clim1fr1  40336  liminfgf  40493  limsup10ex  40508  liminf10ex  40509  dvsinax  40630  wallispilem5  40789  wallispi  40790  stirlinglem5  40798  stirlinglem13  40806  stirlinglem14  40807  stirlinglem15  40808  stirlingr  40810  fourierdlem43  40870  fourierdlem57  40883  fourierdlem58  40884  fourierdlem62  40888  fouriersw  40951  0ome  41249  fmtnof1  41957  prmdvdsfmtnof  42008  sprsymrelf  42255  uspgrsprf  42264