Theorem fmpti 7109

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∀wral 3062   ↦ cmpt 5231  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6543  df-fn 6544  df-f 6545

This theorem is referenced by:  harf  9550  r0weon  10004  dfac2a  10121  ackbij1lem10  10221  cff  10240  isf32lem9  10353  fin1a2lem2  10393  fin1a2lem4  10395  facmapnn  14242  wwlktovf  14904  cjf  15048  ref  15056  imf  15057  absf  15281  limsupcl  15414  limsupgf  15416  eff  16022  sinf  16064  cosf  16065  bitsf  16365  fnum  16675  fden  16676  prmgapprmo  16992  setcepi  18035  catcfuccl  18066  catcfucclOLD  18067  smndex1ibas  18778  smndex2dbas  18792  smndex2hbas  18794  staffval  20448  ocvfval  21211  pjfval  21253  pjpm  21255  leordtval2  22708  lecldbas  22715  nmfval  24089  nmoffn  24220  nmofval  24223  divcn  24376  xrhmeo  24454  tcphex  24726  tchnmfval  24737  ioorf  25082  dveflem  25488  tdeglem1  25565  resinf1o  26037  efifo  26048  logcnlem5  26146  resqrtcn  26247  asinf  26367  acosf  26369  atanf  26375  leibpilem2  26436  areaf  26456  emcllem1  26490  igamf  26545  chtf  26602  chpf  26617  ppif  26624  muf  26634  bposlem7  26783  2lgslem1b  26885  pntrf  27056  pntrsumo1  27058  pntsf  27066  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  oldf  27342  newf  27343  leftf  27350  rightf  27351  normf  30364  hosubcli  31010  cnlnadjlem4  31311  cnlnadjlem6  31313  eulerpartlemsf  33347  fiblem  33386  signsvvf  33579  derangf  34148  snmlff  34309  ex-sategoelel12  34407  sinccvglem  34646  circum  34648  gg-divcn  35152  dnif  35339  f1omptsnlem  36206  phpreu  36461  poimirlem26  36503  cncfres  36622  lsatset  37849  clsk1independent  42783  lhe4.4ex1a  43074  absfico  43903  clim1fr1  44304  liminfgf  44461  limsup10ex  44476  liminf10ex  44477  dvsinax  44616  wallispilem5  44772  wallispi  44773  stirlinglem5  44781  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  stirlingr  44793  fourierdlem43  44853  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fouriersw  44934  0ome  45232  sprsymrelf  46150  fmtnof1  46190  prmdvdsfmtnof  46241  uspgrsprf  46511  ackendofnn0  47324