Theorem fmpti 7131

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∀wral 3058   ↦ cmpt 5230  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  harf  9595  r0weon  10049  dfac2a  10167  ackbij1lem10  10265  cff  10285  isf32lem9  10398  fin1a2lem2  10438  fin1a2lem4  10440  facmapnn  14320  wwlktovf  14991  cjf  15139  ref  15147  imf  15148  absf  15372  limsupcl  15505  limsupgf  15507  eff  16113  sinf  16156  cosf  16157  bitsf  16460  fnum  16775  fden  16776  prmgapprmo  17095  setcepi  18141  catcfuccl  18172  catcfucclOLD  18173  smndex1ibas  18925  smndex2dbas  18939  smndex2hbas  18941  staffval  20858  ocvfval  21701  pjfval  21743  pjpm  21745  psdmul  22187  leordtval2  23235  lecldbas  23242  nmfval  24616  nmoffn  24747  nmofval  24750  divcnOLD  24903  divcn  24905  xrhmeo  24990  tcphex  25264  tchnmfval  25275  ioorf  25621  dveflem  26031  tdeglem1  26111  resinf1o  26592  efifo  26603  logcnlem5  26702  resqrtcn  26806  asinf  26929  acosf  26931  atanf  26937  leibpilem2  26998  areaf  27018  emcllem1  27053  igamf  27108  chtf  27165  chpf  27180  ppif  27187  muf  27197  bposlem7  27348  2lgslem1b  27450  pntrf  27621  pntrsumo1  27623  pntsf  27631  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  oldf  27910  newf  27911  leftf  27918  rightf  27919  normf  31151  hosubcli  31797  cnlnadjlem4  32098  cnlnadjlem6  32100  zringfrac  33561  eulerpartlemsf  34340  fiblem  34379  signsvvf  34572  derangf  35152  snmlff  35313  ex-sategoelel12  35411  sinccvglem  35656  circum  35658  dnif  36456  f1omptsnlem  37318  phpreu  37590  poimirlem26  37632  cncfres  37751  lsatset  38971  clsk1independent  44035  lhe4.4ex1a  44324  absfico  45160  clim1fr1  45556  liminfgf  45713  limsup10ex  45728  liminf10ex  45729  dvsinax  45868  wallispilem5  46024  wallispi  46025  stirlinglem5  46033  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  stirlingr  46045  fourierdlem43  46105  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fouriersw  46186  0ome  46484  sprsymrelf  47419  fmtnof1  47459  prmdvdsfmtnof  47510  uspgrsprf  47989  ackendofnn0  48533