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

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

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  harf  9475  r0weon  9934  dfac2a  10052  ackbij1lem10  10150  cff  10170  isf32lem9  10283  fin1a2lem2  10323  fin1a2lem4  10325  facmapnn  14220  wwlktovf  14891  cjf  15039  ref  15047  imf  15048  absf  15273  limsupcl  15408  limsupgf  15410  eff  16016  sinf  16061  cosf  16062  bitsf  16366  fnum  16681  fden  16682  prmgapprmo  17002  setcepi  18024  catcfuccl  18054  smndex1ibas  18837  smndex2dbas  18851  smndex2hbas  18853  staffval  20786  ocvfval  21633  pjfval  21673  pjpm  21675  psdmul  22121  psdmvr  22124  leordtval2  23168  lecldbas  23175  nmfval  24544  nmoffn  24667  nmofval  24670  divcnOLD  24825  divcn  24827  xrhmeo  24912  tcphex  25185  tchnmfval  25196  ioorf  25542  dveflem  25951  tdeglem1  26031  resinf1o  26513  efifo  26524  logcnlem5  26623  resqrtcn  26727  asinf  26850  acosf  26852  atanf  26858  leibpilem2  26919  areaf  26939  emcllem1  26974  igamf  27029  chtf  27086  chpf  27101  ppif  27108  muf  27118  bposlem7  27269  2lgslem1b  27371  pntrf  27542  pntrsumo1  27544  pntsf  27552  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  oldf  27845  newf  27846  leftf  27863  rightf  27864  normf  31211  hosubcli  31857  cnlnadjlem4  32158  cnlnadjlem6  32160  zringfrac  33647  eulerpartlemsf  34537  fiblem  34576  signsvvf  34757  derangf  35384  snmlff  35545  ex-sategoelel12  35643  sinccvglem  35888  circum  35890  dnif  36696  bj-evalf  37327  f1omptsnlem  37591  phpreu  37855  poimirlem26  37897  cncfres  38016  lsatset  39366  clsk1independent  44402  lhe4.4ex1a  44685  absfico  45576  clim1fr1  45961  liminfgf  46116  limsup10ex  46131  liminf10ex  46132  dvsinax  46271  wallispilem5  46427  wallispi  46428  stirlinglem5  46436  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  stirlingr  46448  fourierdlem43  46508  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fouriersw  46589  0ome  46887  sprsymrelf  47855  fmtnof1  47895  prmdvdsfmtnof  47946  uspgrsprf  48506  ackendofnn0  49044