Theorem fmpti 7066

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ↦ cmpt 5183  ⟶wf 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  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 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  harf  9487  r0weon  9941  dfac2a  10059  ackbij1lem10  10157  cff  10177  isf32lem9  10290  fin1a2lem2  10330  fin1a2lem4  10332  facmapnn  14226  wwlktovf  14898  cjf  15046  ref  15054  imf  15055  absf  15280  limsupcl  15415  limsupgf  15417  eff  16023  sinf  16068  cosf  16069  bitsf  16373  fnum  16688  fden  16689  prmgapprmo  17009  setcepi  18026  catcfuccl  18056  smndex1ibas  18803  smndex2dbas  18817  smndex2hbas  18819  staffval  20726  ocvfval  21551  pjfval  21591  pjpm  21593  psdmul  22029  psdmvr  22032  leordtval2  23075  lecldbas  23082  nmfval  24452  nmoffn  24575  nmofval  24578  divcnOLD  24733  divcn  24735  xrhmeo  24820  tcphex  25093  tchnmfval  25104  ioorf  25450  dveflem  25859  tdeglem1  25939  resinf1o  26421  efifo  26432  logcnlem5  26531  resqrtcn  26635  asinf  26758  acosf  26760  atanf  26766  leibpilem2  26827  areaf  26847  emcllem1  26882  igamf  26937  chtf  26994  chpf  27009  ppif  27016  muf  27026  bposlem7  27177  2lgslem1b  27279  pntrf  27450  pntrsumo1  27452  pntsf  27460  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  oldf  27741  newf  27742  leftf  27753  rightf  27754  normf  31025  hosubcli  31671  cnlnadjlem4  31972  cnlnadjlem6  31974  zringfrac  33498  eulerpartlemsf  34323  fiblem  34362  signsvvf  34543  derangf  35128  snmlff  35289  ex-sategoelel12  35387  sinccvglem  35632  circum  35634  dnif  36435  f1omptsnlem  37297  phpreu  37571  poimirlem26  37613  cncfres  37732  lsatset  38956  clsk1independent  44008  lhe4.4ex1a  44291  absfico  45185  clim1fr1  45572  liminfgf  45729  limsup10ex  45744  liminf10ex  45745  dvsinax  45884  wallispilem5  46040  wallispi  46041  stirlinglem5  46049  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  stirlingr  46061  fourierdlem43  46121  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fouriersw  46202  0ome  46500  sprsymrelf  47469  fmtnof1  47509  prmdvdsfmtnof  47560  uspgrsprf  48107  ackendofnn0  48646