Theorem fmpti 6862

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3138   ↦ cmpt 5132  ⟶wf 6337

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-fv 6349

This theorem is referenced by:  harf  9010  r0weon  9424  dfac2a  9541  ackbij1lem10  9637  cff  9656  isf32lem9  9769  fin1a2lem2  9809  fin1a2lem4  9811  facmapnn  13635  wwlktovf  14305  cjf  14448  ref  14456  imf  14457  absf  14682  limsupcl  14815  limsupgf  14817  eff  15420  sinf  15462  cosf  15463  bitsf  15759  fnum  16065  fden  16066  prmgapprmo  16381  setcepi  17331  catcfuccl  17352  smndex1ibas  18048  smndex2dbas  18062  smndex2hbas  18064  staffval  19601  ocvfval  20793  pjfval  20833  pjpm  20835  leordtval2  21803  lecldbas  21810  nmfval  23181  nmoffn  23303  nmofval  23306  divcn  23459  xrhmeo  23533  tcphex  23803  tchnmfval  23814  ioorf  24157  dveflem  24561  resinf1o  25106  efifo  25117  logcnlem5  25215  resqrtcn  25316  asinf  25436  acosf  25438  atanf  25444  leibpilem2  25505  areaf  25525  emcllem1  25559  igamf  25614  chtf  25671  chpf  25686  ppif  25693  muf  25703  bposlem7  25852  2lgslem1b  25954  pntrf  26125  pntrsumo1  26127  pntsf  26135  pntrlog2bndlem4  26142  pntrlog2bndlem5  26143  normf  28884  hosubcli  29530  cnlnadjlem4  29831  cnlnadjlem6  29833  eulerpartlemsf  31624  fiblem  31663  signsvvf  31856  derangf  32422  snmlff  32583  ex-sategoelel12  32681  sinccvglem  32922  circum  32924  dnif  33820  f1omptsnlem  34633  phpreu  34910  poimirlem26  34952  cncfres  35075  lsatset  36158  clsk1independent  40486  lhe4.4ex1a  40751  absfico  41571  clim1fr1  41972  liminfgf  42129  limsup10ex  42144  liminf10ex  42145  dvsinax  42287  wallispilem5  42444  wallispi  42445  stirlinglem5  42453  stirlinglem13  42461  stirlinglem14  42462  stirlinglem15  42463  stirlingr  42465  fourierdlem43  42525  fourierdlem57  42538  fourierdlem58  42539  fourierdlem62  42543  fouriersw  42606  0ome  42901  sprsymrelf  43742  fmtnof1  43782  prmdvdsfmtnof  43833  uspgrsprf  44106