Theorem fmpti 7146

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∀wral 3067   ↦ cmpt 5249  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  harf  9627  r0weon  10081  dfac2a  10199  ackbij1lem10  10297  cff  10317  isf32lem9  10430  fin1a2lem2  10470  fin1a2lem4  10472  facmapnn  14334  wwlktovf  15005  cjf  15153  ref  15161  imf  15162  absf  15386  limsupcl  15519  limsupgf  15521  eff  16129  sinf  16172  cosf  16173  bitsf  16473  fnum  16789  fden  16790  prmgapprmo  17109  setcepi  18155  catcfuccl  18186  catcfucclOLD  18187  smndex1ibas  18935  smndex2dbas  18949  smndex2hbas  18951  staffval  20864  ocvfval  21707  pjfval  21749  pjpm  21751  psdmul  22193  leordtval2  23241  lecldbas  23248  nmfval  24622  nmoffn  24753  nmofval  24756  divcnOLD  24909  divcn  24911  xrhmeo  24996  tcphex  25270  tchnmfval  25281  ioorf  25627  dveflem  26037  tdeglem1  26117  resinf1o  26596  efifo  26607  logcnlem5  26706  resqrtcn  26810  asinf  26933  acosf  26935  atanf  26941  leibpilem2  27002  areaf  27022  emcllem1  27057  igamf  27112  chtf  27169  chpf  27184  ppif  27191  muf  27201  bposlem7  27352  2lgslem1b  27454  pntrf  27625  pntrsumo1  27627  pntsf  27635  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  oldf  27914  newf  27915  leftf  27922  rightf  27923  normf  31155  hosubcli  31801  cnlnadjlem4  32102  cnlnadjlem6  32104  zringfrac  33547  eulerpartlemsf  34324  fiblem  34363  signsvvf  34556  derangf  35136  snmlff  35297  ex-sategoelel12  35395  sinccvglem  35640  circum  35642  dnif  36440  f1omptsnlem  37302  phpreu  37564  poimirlem26  37606  cncfres  37725  lsatset  38946  clsk1independent  44008  lhe4.4ex1a  44298  absfico  45125  clim1fr1  45522  liminfgf  45679  limsup10ex  45694  liminf10ex  45695  dvsinax  45834  wallispilem5  45990  wallispi  45991  stirlinglem5  45999  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  stirlingr  46011  fourierdlem43  46071  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fouriersw  46152  0ome  46450  sprsymrelf  47369  fmtnof1  47409  prmdvdsfmtnof  47460  uspgrsprf  47869  ackendofnn0  48418