Theorem fmpti 7111

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3081   ↦ cmpt 5194  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  harf  9527  r0weon  10012  dfac2a  10129  ackbij1lem10  10227  cff  10246  isf32lem9  10360  fin1a2lem2  10400  fin1a2lem4  10402  facmapnn  14339  wwlktovf  15017  cjf  15179  ref  15187  imf  15188  absf  15413  limsupcl  15548  limsupgf  15550  eff  16157  sinf  16202  cosf  16203  bitsf  16507  fnum  16823  fden  16824  prmgapprmo  17144  setcepi  18167  catcfuccl  18197  smndex1ibas  18996  smndex2dbas  19013  smndex2hbas  19015  staffval  20994  ocvfval  21866  pjfval  21906  pjpm  21908  psdmul  22379  psdmvr  22382  leordtval2  23419  lecldbas  23426  nmfval  24796  nmoffn  24919  nmofval  24922  divcn  25078  xrhmeo  25156  tcphex  25427  tchnmfval  25438  ioorf  25783  dveflem  26189  tdeglem1  26266  resinf1o  26752  efifo  26763  logcnlem5  26862  resqrtcn  26965  asinf  27088  acosf  27090  atanf  27096  leibpilem2  27157  areaf  27177  emcllem1  27211  igamf  27266  chtf  27323  chpf  27338  ppif  27345  muf  27355  bposlem7  27505  2lgslem1b  27607  pntrf  27778  pntrsumo1  27780  pntsf  27788  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  oldf  28081  newf  28082  leftf  28099  rightf  28100  normf  31546  hosubcli  32192  cnlnadjlem4  32493  cnlnadjlem6  32495  zringfrac  33908  eulerpartlemsf  34814  fiblem  34853  signsvvf  35031  derangf  35697  snmlff  35858  ex-sategoelel12  35956  sinccvglem  36201  circum  36203  dnif  37120  bj-evalf  37773  f1omptsnlem  38039  phpreu  38312  poimirlem26  38354  cncfres  38474  lsatset  39822  clsk1independent  44830  lhe4.4ex1a  45097  absfico  45992  clim1fr1  46375  liminfgf  46530  limsup10ex  46545  liminf10ex  46546  dvsinax  46685  wallispilem5  46841  wallispi  46842  stirlinglem5  46850  stirlinglem13  46858  stirlinglem14  46859  stirlinglem15  46860  stirlingr  46862  fourierdlem43  46922  fourierdlem57  46935  fourierdlem58  46936  fourierdlem62  46940  fouriersw  47003  0ome  47301  sprsymrelf  48302  fmtnof1  48345  prmdvdsfmtnof  48396  uspgrsprf  48969  ackendofnn0  49521