Theorem fmpti 7059

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5167  ⟶wf 6489

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 2709  ax-sep 5232  ax-pr 5371

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  harf  9467  r0weon  9928  dfac2a  10046  ackbij1lem10  10144  cff  10164  isf32lem9  10277  fin1a2lem2  10317  fin1a2lem4  10319  facmapnn  14241  wwlktovf  14912  cjf  15060  ref  15068  imf  15069  absf  15294  limsupcl  15429  limsupgf  15431  eff  16040  sinf  16085  cosf  16086  bitsf  16390  fnum  16706  fden  16707  prmgapprmo  17027  setcepi  18049  catcfuccl  18079  smndex1ibas  18862  smndex2dbas  18879  smndex2hbas  18881  staffval  20812  ocvfval  21659  pjfval  21699  pjpm  21701  psdmul  22145  psdmvr  22148  leordtval2  23190  lecldbas  23197  nmfval  24566  nmoffn  24689  nmofval  24692  divcn  24848  xrhmeo  24926  tcphex  25197  tchnmfval  25208  ioorf  25553  dveflem  25959  tdeglem1  26036  resinf1o  26516  efifo  26527  logcnlem5  26626  resqrtcn  26729  asinf  26852  acosf  26854  atanf  26860  leibpilem2  26921  areaf  26941  emcllem1  26976  igamf  27031  chtf  27088  chpf  27103  ppif  27110  muf  27120  bposlem7  27270  2lgslem1b  27372  pntrf  27543  pntrsumo1  27545  pntsf  27553  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  oldf  27846  newf  27847  leftf  27864  rightf  27865  normf  31212  hosubcli  31858  cnlnadjlem4  32159  cnlnadjlem6  32161  zringfrac  33632  eulerpartlemsf  34522  fiblem  34561  signsvvf  34742  derangf  35369  snmlff  35530  ex-sategoelel12  35628  sinccvglem  35873  circum  35875  dnif  36753  bj-evalf  37405  f1omptsnlem  37669  phpreu  37942  poimirlem26  37984  cncfres  38103  lsatset  39453  clsk1independent  44494  lhe4.4ex1a  44777  absfico  45668  clim1fr1  46052  liminfgf  46207  limsup10ex  46222  liminf10ex  46223  dvsinax  46362  wallispilem5  46518  wallispi  46519  stirlinglem5  46527  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  stirlingr  46539  fourierdlem43  46599  fourierdlem57  46612  fourierdlem58  46613  fourierdlem62  46617  fouriersw  46680  0ome  46978  sprsymrelf  47970  fmtnof1  48013  prmdvdsfmtnof  48064  uspgrsprf  48637  ackendofnn0  49175