Theorem fmpti 7087

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3045   ↦ cmpt 5191  ⟶wf 6510

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  harf  9518  r0weon  9972  dfac2a  10090  ackbij1lem10  10188  cff  10208  isf32lem9  10321  fin1a2lem2  10361  fin1a2lem4  10363  facmapnn  14257  wwlktovf  14929  cjf  15077  ref  15085  imf  15086  absf  15311  limsupcl  15446  limsupgf  15448  eff  16054  sinf  16099  cosf  16100  bitsf  16404  fnum  16719  fden  16720  prmgapprmo  17040  setcepi  18057  catcfuccl  18087  smndex1ibas  18834  smndex2dbas  18848  smndex2hbas  18850  staffval  20757  ocvfval  21582  pjfval  21622  pjpm  21624  psdmul  22060  psdmvr  22063  leordtval2  23106  lecldbas  23113  nmfval  24483  nmoffn  24606  nmofval  24609  divcnOLD  24764  divcn  24766  xrhmeo  24851  tcphex  25124  tchnmfval  25135  ioorf  25481  dveflem  25890  tdeglem1  25970  resinf1o  26452  efifo  26463  logcnlem5  26562  resqrtcn  26666  asinf  26789  acosf  26791  atanf  26797  leibpilem2  26858  areaf  26878  emcllem1  26913  igamf  26968  chtf  27025  chpf  27040  ppif  27047  muf  27057  bposlem7  27208  2lgslem1b  27310  pntrf  27481  pntrsumo1  27483  pntsf  27491  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  oldf  27772  newf  27773  leftf  27784  rightf  27785  normf  31059  hosubcli  31705  cnlnadjlem4  32006  cnlnadjlem6  32008  zringfrac  33532  eulerpartlemsf  34357  fiblem  34396  signsvvf  34577  derangf  35162  snmlff  35323  ex-sategoelel12  35421  sinccvglem  35666  circum  35668  dnif  36469  f1omptsnlem  37331  phpreu  37605  poimirlem26  37647  cncfres  37766  lsatset  38990  clsk1independent  44042  lhe4.4ex1a  44325  absfico  45219  clim1fr1  45606  liminfgf  45763  limsup10ex  45778  liminf10ex  45779  dvsinax  45918  wallispilem5  46074  wallispi  46075  stirlinglem5  46083  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  fourierdlem43  46155  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fouriersw  46236  0ome  46534  sprsymrelf  47500  fmtnof1  47540  prmdvdsfmtnof  47591  uspgrsprf  48138  ackendofnn0  48677