Theorem fmpti 7131

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  ∀wral 3054   ↦ cmpt 5239  ⟶wf 6554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-fun 6560  df-fn 6561  df-f 6562

This theorem is referenced by:  harf  9608  r0weon  10062  dfac2a  10180  ackbij1lem10  10278  cff  10298  isf32lem9  10411  fin1a2lem2  10451  fin1a2lem4  10453  facmapnn  14314  wwlktovf  14986  cjf  15130  ref  15138  imf  15139  absf  15363  limsupcl  15496  limsupgf  15498  eff  16104  sinf  16147  cosf  16148  bitsf  16448  fnum  16765  fden  16766  prmgapprmo  17085  setcepi  18131  catcfuccl  18162  catcfucclOLD  18163  smndex1ibas  18911  smndex2dbas  18925  smndex2hbas  18927  staffval  20842  ocvfval  21684  pjfval  21726  pjpm  21728  psdmul  22182  leordtval2  23230  lecldbas  23237  nmfval  24611  nmoffn  24742  nmofval  24745  divcnOLD  24898  divcn  24900  xrhmeo  24985  tcphex  25259  tchnmfval  25270  ioorf  25616  dveflem  26025  tdeglem1  26105  resinf1o  26586  efifo  26597  logcnlem5  26696  resqrtcn  26800  asinf  26923  acosf  26925  atanf  26931  leibpilem2  26992  areaf  27012  emcllem1  27047  igamf  27102  chtf  27159  chpf  27174  ppif  27181  muf  27191  bposlem7  27342  2lgslem1b  27444  pntrf  27615  pntrsumo1  27617  pntsf  27625  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  oldf  27904  newf  27905  leftf  27912  rightf  27913  normf  31079  hosubcli  31725  cnlnadjlem4  32026  cnlnadjlem6  32028  zringfrac  33460  eulerpartlemsf  34231  fiblem  34270  signsvvf  34463  derangf  35034  snmlff  35195  ex-sategoelel12  35293  sinccvglem  35538  circum  35540  dnif  36216  f1omptsnlem  37081  phpreu  37343  poimirlem26  37385  cncfres  37504  lsatset  38726  clsk1independent  43775  lhe4.4ex1a  44065  absfico  44886  clim1fr1  45283  liminfgf  45440  limsup10ex  45455  liminf10ex  45456  dvsinax  45595  wallispilem5  45751  wallispi  45752  stirlinglem5  45760  stirlinglem13  45768  stirlinglem14  45769  stirlinglem15  45770  stirlingr  45772  fourierdlem43  45832  fourierdlem57  45845  fourierdlem58  45846  fourierdlem62  45850  fouriersw  45913  0ome  46211  sprsymrelf  47128  fmtnof1  47168  prmdvdsfmtnof  47219  uspgrsprf  47595  ackendofnn0  48144