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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078   ↦ cmpt 5190  ⟶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 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  harf  9533  r0weon  10018  dfac2a  10135  ackbij1lem10  10233  cff  10252  isf32lem9  10366  fin1a2lem2  10406  fin1a2lem4  10408  facmapnn  14351  wwlktovf  15031  cjf  15193  ref  15201  imf  15202  absf  15427  limsupcl  15562  limsupgf  15564  eff  16171  sinf  16216  cosf  16217  bitsf  16521  fnum  16837  fden  16838  prmgapprmo  17158  setcepi  18181  catcfuccl  18211  smndex1ibas  19013  smndex2dbas  19030  smndex2hbas  19032  staffval  21011  ocvfval  21883  pjfval  21923  pjpm  21925  psdmul  22398  psdmvr  22401  leordtval2  23441  lecldbas  23448  nmfval  24818  nmoffn  24941  nmofval  24944  divcn  25100  xrhmeo  25178  tcphex  25449  tchnmfval  25460  ioorf  25805  dveflem  26211  tdeglem1  26288  resinf1o  26774  efifo  26785  logcnlem5  26884  resqrtcn  26987  asinf  27110  acosf  27112  atanf  27118  leibpilem2  27179  areaf  27199  emcllem1  27233  igamf  27288  chtf  27345  chpf  27360  ppif  27367  muf  27377  bposlem7  27527  2lgslem1b  27629  pntrf  27800  pntrsumo1  27802  pntsf  27810  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  oldf  28103  newf  28104  leftf  28121  rightf  28122  normf  31605  hosubcli  32251  cnlnadjlem4  32552  cnlnadjlem6  32554  zringfrac  33966  eulerpartlemsf  34872  fiblem  34911  signsvvf  35089  derangf  35749  snmlff  35910  ex-sategoelel12  36008  sinccvglem  36253  circum  36255  dnif  37173  bj-evalf  37826  f1omptsnlem  38092  phpreu  38360  poimirlem26  38397  cncfres  38517  lsatset  39865  clsk1independent  44888  lhe4.4ex1a  45155  absfico  46050  clim1fr1  46433  liminfgf  46588  limsup10ex  46603  liminf10ex  46604  dvsinax  46743  wallispilem5  46899  wallispi  46900  stirlinglem5  46908  stirlinglem13  46916  stirlinglem14  46917  stirlinglem15  46918  stirlingr  46920  fourierdlem43  46980  fourierdlem57  46993  fourierdlem58  46994  fourierdlem62  46998  fouriersw  47061  0ome  47359  sinnpoly  47761  sprsymrelf  48397  fmtnof1  48440  prmdvdsfmtnof  48491  uspgrsprf  49064  ackendofnn0  49616  dvsec  50691  dvcsc  50692  dvcot  50693