Theorem fmpti 7064

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3051   ↦ cmpt 5166  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  harf  9473  r0weon  9934  dfac2a  10052  ackbij1lem10  10150  cff  10170  isf32lem9  10283  fin1a2lem2  10323  fin1a2lem4  10325  facmapnn  14247  wwlktovf  14918  cjf  15066  ref  15074  imf  15075  absf  15300  limsupcl  15435  limsupgf  15437  eff  16046  sinf  16091  cosf  16092  bitsf  16396  fnum  16712  fden  16713  prmgapprmo  17033  setcepi  18055  catcfuccl  18085  smndex1ibas  18868  smndex2dbas  18885  smndex2hbas  18887  staffval  20818  ocvfval  21646  pjfval  21686  pjpm  21688  psdmul  22132  psdmvr  22135  leordtval2  23177  lecldbas  23184  nmfval  24553  nmoffn  24676  nmofval  24679  divcn  24835  xrhmeo  24913  tcphex  25184  tchnmfval  25195  ioorf  25540  dveflem  25946  tdeglem1  26023  resinf1o  26500  efifo  26511  logcnlem5  26610  resqrtcn  26713  asinf  26836  acosf  26838  atanf  26844  leibpilem2  26905  areaf  26925  emcllem1  26959  igamf  27014  chtf  27071  chpf  27086  ppif  27093  muf  27103  bposlem7  27253  2lgslem1b  27355  pntrf  27526  pntrsumo1  27528  pntsf  27536  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  oldf  27829  newf  27830  leftf  27847  rightf  27848  normf  31194  hosubcli  31840  cnlnadjlem4  32141  cnlnadjlem6  32143  zringfrac  33614  eulerpartlemsf  34503  fiblem  34542  signsvvf  34723  derangf  35350  snmlff  35511  ex-sategoelel12  35609  sinccvglem  35854  circum  35856  dnif  36734  bj-evalf  37386  f1omptsnlem  37652  phpreu  37925  poimirlem26  37967  cncfres  38086  lsatset  39436  clsk1independent  44473  lhe4.4ex1a  44756  absfico  45647  clim1fr1  46031  liminfgf  46186  limsup10ex  46201  liminf10ex  46202  dvsinax  46341  wallispilem5  46497  wallispi  46498  stirlinglem5  46506  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  fourierdlem43  46578  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fouriersw  46659  0ome  46957  sprsymrelf  47955  fmtnof1  47998  prmdvdsfmtnof  48049  uspgrsprf  48622  ackendofnn0  49160