Theorem fmpti 7144

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∀wral 3080   ↦ cmpt 5192  ⟶wf 6562

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  harf  9589  r0weon  10130  dfac2a  10247  ackbij1lem10  10345  cff  10364  isf32lem9  10478  fin1a2lem2  10518  fin1a2lem4  10520  facmapnn  14470  wwlktovf  15152  cjf  15314  ref  15322  imf  15323  absf  15548  limsupcl  15684  limsupgf  15686  eff  16291  sinf  16336  cosf  16337  bitsf  16641  fnum  16962  fden  16963  prmgapprmo  17284  setcepi  18313  catcfuccl  18343  smndex1ibas  19146  smndex2dbas  19163  smndex2hbas  19165  staffval  21149  ocvfval  22027  pjfval  22067  pjpm  22069  psdmul  22542  psdmvr  22545  leordtval2  23585  lecldbas  23592  nmfval  24962  nmoffn  25085  nmofval  25088  divcn  25244  xrhmeo  25322  tcphex  25593  tchnmfval  25604  ioorf  25949  dveflem  26354  tdeglem1  26431  resinf1o  26921  efifo  26932  logcnlem5  27031  resqrtcn  27134  asinf  27257  acosf  27259  atanf  27265  leibpilem2  27326  areaf  27346  emcllem1  27380  igamf  27435  chtf  27492  chpf  27507  ppif  27514  muf  27524  bposlem7  27674  2lgslem1b  27776  pntrf  27947  pntrsumo1  27949  pntsf  27957  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  oldf  28280  newf  28281  leftf  28298  rightf  28299  normf  31782  hosubcli  32428  cnlnadjlem4  32729  cnlnadjlem6  32731  zzedom  33958  zringfrac  34189  eulerpartlemsf  35102  fiblem  35141  signsvvf  35319  j00smo  36046  derangf  36141  snmlff  36302  ex-sategoelel12  36400  sinccvglem  36645  circum  36647  dnif  37555  bj-evalf  38265  f1omptsnlem  38527  phpreu  38795  poimirlem26  38832  cncfres  38965  lsatset  40313  clsk1independent  45307  lhe4.4ex1a  45574  absfico  46504  clim1fr1  46886  liminfgf  47041  limsup10ex  47056  liminf10ex  47057  dvsinax  47196  wallispilem5  47352  wallispi  47353  stirlinglem5  47361  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  stirlingr  47373  fourierdlem43  47433  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fouriersw  47514  0ome  47812  sinnpoly  48214  sprsymrelf  48850  fmtnof1  48893  prmdvdsfmtnof  48944  uspgrsprf  49517  ackendofnn0  50127  sinhf  51239  coshf  51243  tanhf  51249  dvsec  51284  dvcsc  51285  dvcot  51286