Theorem fmpti 7046

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

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

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486

This theorem is referenced by:  harf  9450  r0weon  9906  dfac2a  10024  ackbij1lem10  10122  cff  10142  isf32lem9  10255  fin1a2lem2  10295  fin1a2lem4  10297  facmapnn  14192  wwlktovf  14863  cjf  15011  ref  15019  imf  15020  absf  15245  limsupcl  15380  limsupgf  15382  eff  15988  sinf  16033  cosf  16034  bitsf  16338  fnum  16653  fden  16654  prmgapprmo  16974  setcepi  17995  catcfuccl  18025  smndex1ibas  18774  smndex2dbas  18788  smndex2hbas  18790  staffval  20726  ocvfval  21573  pjfval  21613  pjpm  21615  psdmul  22051  psdmvr  22054  leordtval2  23097  lecldbas  23104  nmfval  24474  nmoffn  24597  nmofval  24600  divcnOLD  24755  divcn  24757  xrhmeo  24842  tcphex  25115  tchnmfval  25126  ioorf  25472  dveflem  25881  tdeglem1  25961  resinf1o  26443  efifo  26454  logcnlem5  26553  resqrtcn  26657  asinf  26780  acosf  26782  atanf  26788  leibpilem2  26849  areaf  26869  emcllem1  26904  igamf  26959  chtf  27016  chpf  27031  ppif  27038  muf  27048  bposlem7  27199  2lgslem1b  27301  pntrf  27472  pntrsumo1  27474  pntsf  27482  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  oldf  27767  newf  27768  leftf  27779  rightf  27780  normf  31067  hosubcli  31713  cnlnadjlem4  32014  cnlnadjlem6  32016  zringfrac  33491  eulerpartlemsf  34327  fiblem  34366  signsvvf  34547  derangf  35141  snmlff  35302  ex-sategoelel12  35400  sinccvglem  35645  circum  35647  dnif  36448  f1omptsnlem  37310  phpreu  37584  poimirlem26  37626  cncfres  37745  lsatset  38969  clsk1independent  44019  lhe4.4ex1a  44302  absfico  45196  clim1fr1  45582  liminfgf  45739  limsup10ex  45754  liminf10ex  45755  dvsinax  45894  wallispilem5  46050  wallispi  46051  stirlinglem5  46059  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  stirlingr  46071  fourierdlem43  46131  fourierdlem57  46144  fourierdlem58  46145  fourierdlem62  46149  fouriersw  46212  0ome  46510  sprsymrelf  47479  fmtnof1  47519  prmdvdsfmtnof  47570  uspgrsprf  48130  ackendofnn0  48669