Theorem fmpti 7132

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061   ↦ cmpt 5225  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  harf  9598  r0weon  10052  dfac2a  10170  ackbij1lem10  10268  cff  10288  isf32lem9  10401  fin1a2lem2  10441  fin1a2lem4  10443  facmapnn  14324  wwlktovf  14995  cjf  15143  ref  15151  imf  15152  absf  15376  limsupcl  15509  limsupgf  15511  eff  16117  sinf  16160  cosf  16161  bitsf  16464  fnum  16779  fden  16780  prmgapprmo  17100  setcepi  18133  catcfuccl  18163  smndex1ibas  18913  smndex2dbas  18927  smndex2hbas  18929  staffval  20842  ocvfval  21684  pjfval  21726  pjpm  21728  psdmul  22170  psdmvr  22173  leordtval2  23220  lecldbas  23227  nmfval  24601  nmoffn  24732  nmofval  24735  divcnOLD  24890  divcn  24892  xrhmeo  24977  tcphex  25251  tchnmfval  25262  ioorf  25608  dveflem  26017  tdeglem1  26097  resinf1o  26578  efifo  26589  logcnlem5  26688  resqrtcn  26792  asinf  26915  acosf  26917  atanf  26923  leibpilem2  26984  areaf  27004  emcllem1  27039  igamf  27094  chtf  27151  chpf  27166  ppif  27173  muf  27183  bposlem7  27334  2lgslem1b  27436  pntrf  27607  pntrsumo1  27609  pntsf  27617  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  oldf  27896  newf  27897  leftf  27904  rightf  27905  normf  31142  hosubcli  31788  cnlnadjlem4  32089  cnlnadjlem6  32091  zringfrac  33582  eulerpartlemsf  34361  fiblem  34400  signsvvf  34594  derangf  35173  snmlff  35334  ex-sategoelel12  35432  sinccvglem  35677  circum  35679  dnif  36475  f1omptsnlem  37337  phpreu  37611  poimirlem26  37653  cncfres  37772  lsatset  38991  clsk1independent  44059  lhe4.4ex1a  44348  absfico  45223  clim1fr1  45616  liminfgf  45773  limsup10ex  45788  liminf10ex  45789  dvsinax  45928  wallispilem5  46084  wallispi  46085  stirlinglem5  46093  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  fourierdlem43  46165  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fouriersw  46246  0ome  46544  sprsymrelf  47482  fmtnof1  47522  prmdvdsfmtnof  47573  uspgrsprf  48062  ackendofnn0  48605