Theorem fmpti 7110

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ↦ cmpt 5186  ⟶wf 6533

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  harf  9545  r0weon  10084  dfac2a  10201  ackbij1lem10  10299  cff  10318  isf32lem9  10432  fin1a2lem2  10472  fin1a2lem4  10474  facmapnn  14422  wwlktovf  15102  cjf  15264  ref  15272  imf  15273  absf  15498  limsupcl  15633  limsupgf  15635  eff  16240  sinf  16285  cosf  16286  bitsf  16590  fnum  16911  fden  16912  prmgapprmo  17233  setcepi  18256  catcfuccl  18286  smndex1ibas  19089  smndex2dbas  19106  smndex2hbas  19108  staffval  21091  ocvfval  21965  pjfval  22005  pjpm  22007  psdmul  22480  psdmvr  22483  leordtval2  23523  lecldbas  23530  nmfval  24900  nmoffn  25023  nmofval  25026  divcn  25182  xrhmeo  25260  tcphex  25531  tchnmfval  25542  ioorf  25887  dveflem  26292  tdeglem1  26369  resinf1o  26857  efifo  26868  logcnlem5  26967  resqrtcn  27070  asinf  27193  acosf  27195  atanf  27201  leibpilem2  27262  areaf  27282  emcllem1  27316  igamf  27371  chtf  27428  chpf  27443  ppif  27450  muf  27460  bposlem7  27610  2lgslem1b  27712  pntrf  27883  pntrsumo1  27885  pntsf  27893  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  oldf  28216  newf  28217  leftf  28234  rightf  28235  normf  31718  hosubcli  32364  cnlnadjlem4  32665  cnlnadjlem6  32667  zringfrac  34079  eulerpartlemsf  34984  fiblem  35023  signsvvf  35201  derangf  35912  snmlff  36073  ex-sategoelel12  36171  sinccvglem  36416  circum  36418  dnif  37320  bj-evalf  37975  f1omptsnlem  38239  phpreu  38507  poimirlem26  38544  cncfres  38679  lsatset  40027  clsk1independent  45031  lhe4.4ex1a  45298  absfico  46200  clim1fr1  46582  liminfgf  46737  limsup10ex  46752  liminf10ex  46753  dvsinax  46892  wallispilem5  47048  wallispi  47049  stirlinglem5  47057  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  stirlingr  47069  fourierdlem43  47129  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fouriersw  47210  0ome  47508  sinnpoly  47910  sprsymrelf  48546  fmtnof1  48589  prmdvdsfmtnof  48640  uspgrsprf  49213  ackendofnn0  49765  dvsec  50825  dvcsc  50826  dvcot  50827