Theorem fmpti 7096

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3060   ↦ cmpt 5224  ⟶wf 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-fun 6534  df-fn 6535  df-f 6536

This theorem is referenced by:  harf  9535  r0weon  9989  dfac2a  10106  ackbij1lem10  10206  cff  10225  isf32lem9  10338  fin1a2lem2  10378  fin1a2lem4  10380  facmapnn  14227  wwlktovf  14889  cjf  15033  ref  15041  imf  15042  absf  15266  limsupcl  15399  limsupgf  15401  eff  16007  sinf  16049  cosf  16050  bitsf  16350  fnum  16660  fden  16661  prmgapprmo  16977  setcepi  18020  catcfuccl  18051  catcfucclOLD  18052  smndex1ibas  18756  smndex2dbas  18770  smndex2hbas  18772  staffval  20404  ocvfval  21152  pjfval  21194  pjpm  21196  leordtval2  22645  lecldbas  22652  nmfval  24026  nmoffn  24157  nmofval  24160  divcn  24313  xrhmeo  24391  tcphex  24663  tchnmfval  24674  ioorf  25019  dveflem  25425  tdeglem1  25502  resinf1o  25974  efifo  25985  logcnlem5  26083  resqrtcn  26184  asinf  26304  acosf  26306  atanf  26312  leibpilem2  26373  areaf  26393  emcllem1  26427  igamf  26482  chtf  26539  chpf  26554  ppif  26561  muf  26571  bposlem7  26720  2lgslem1b  26822  pntrf  26993  pntrsumo1  26995  pntsf  27003  pntrlog2bndlem4  27010  pntrlog2bndlem5  27011  oldf  27275  newf  27276  leftf  27283  rightf  27284  normf  30239  hosubcli  30885  cnlnadjlem4  31186  cnlnadjlem6  31188  eulerpartlemsf  33189  fiblem  33228  signsvvf  33421  derangf  33990  snmlff  34151  ex-sategoelel12  34249  sinccvglem  34488  circum  34490  dnif  35154  f1omptsnlem  36021  phpreu  36276  poimirlem26  36318  cncfres  36438  lsatset  37665  clsk1independent  42568  lhe4.4ex1a  42859  absfico  43688  clim1fr1  44090  liminfgf  44247  limsup10ex  44262  liminf10ex  44263  dvsinax  44402  wallispilem5  44558  wallispi  44559  stirlinglem5  44567  stirlinglem13  44575  stirlinglem14  44576  stirlinglem15  44577  stirlingr  44579  fourierdlem43  44639  fourierdlem57  44652  fourierdlem58  44653  fourierdlem62  44657  fouriersw  44720  0ome  45018  sprsymrelf  45935  fmtnof1  45975  prmdvdsfmtnof  46026  uspgrsprf  46296  ackendofnn0  47018