Theorem fmpti 7108

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∀wral 3085   ↦ cmpt 5196  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-fun 6539  df-fn 6540  df-f 6541

This theorem is referenced by:  harf  9519  r0weon  9995  dfac2a  10112  ackbij1lem10  10210  cff  10230  isf32lem9  10344  fin1a2lem2  10384  fin1a2lem4  10386  facmapnn  14320  wwlktovf  14992  cjf  15154  ref  15162  imf  15163  absf  15388  limsupcl  15523  limsupgf  15525  eff  16134  sinf  16179  cosf  16180  bitsf  16484  fnum  16800  fden  16801  prmgapprmo  17121  setcepi  18144  catcfuccl  18174  smndex1ibas  18958  smndex2dbas  18975  smndex2hbas  18977  staffval  20921  ocvfval  21784  pjfval  21824  pjpm  21826  psdmul  22297  psdmvr  22300  leordtval2  23337  lecldbas  23344  nmfval  24713  nmoffn  24836  nmofval  24839  divcn  24995  xrhmeo  25073  tcphex  25344  tchnmfval  25355  ioorf  25700  dveflem  26106  tdeglem1  26183  resinf1o  26666  efifo  26677  logcnlem5  26776  resqrtcn  26879  asinf  27002  acosf  27004  atanf  27010  leibpilem2  27071  areaf  27091  emcllem1  27125  igamf  27180  chtf  27237  chpf  27252  ppif  27259  muf  27269  bposlem7  27419  2lgslem1b  27521  pntrf  27692  pntrsumo1  27694  pntsf  27702  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  oldf  27995  newf  27996  leftf  28013  rightf  28014  normf  31415  hosubcli  32061  cnlnadjlem4  32362  cnlnadjlem6  32364  zringfrac  33788  eulerpartlemsf  34693  fiblem  34732  signsvvf  34910  derangf  35558  snmlff  35719  ex-sategoelel12  35817  sinccvglem  36062  circum  36064  dnif  36951  bj-evalf  37603  f1omptsnlem  37869  phpreu  38142  poimirlem26  38184  cncfres  38303  lsatset  39653  clsk1independent  44663  lhe4.4ex1a  44930  absfico  45825  clim1fr1  46208  liminfgf  46363  limsup10ex  46378  liminf10ex  46379  dvsinax  46518  wallispilem5  46674  wallispi  46675  stirlinglem5  46683  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  stirlingr  46695  fourierdlem43  46755  fourierdlem57  46768  fourierdlem58  46769  fourierdlem62  46773  fouriersw  46836  0ome  47134  sprsymrelf  48132  fmtnof1  48175  prmdvdsfmtnof  48226  uspgrsprf  48799  ackendofnn0  49348