Theorem fmpti 7117

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ↦ cmpt 5185  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  harf  9559  r0weon  10098  dfac2a  10215  ackbij1lem10  10313  cff  10332  isf32lem9  10446  fin1a2lem2  10486  fin1a2lem4  10488  facmapnn  14436  wwlktovf  15118  cjf  15280  ref  15288  imf  15289  absf  15514  limsupcl  15649  limsupgf  15651  eff  16256  sinf  16301  cosf  16302  bitsf  16606  fnum  16927  fden  16928  prmgapprmo  17249  setcepi  18272  catcfuccl  18302  smndex1ibas  19105  smndex2dbas  19122  smndex2hbas  19124  staffval  21107  ocvfval  21981  pjfval  22021  pjpm  22023  psdmul  22496  psdmvr  22499  leordtval2  23539  lecldbas  23546  nmfval  24916  nmoffn  25039  nmofval  25042  divcn  25198  xrhmeo  25276  tcphex  25547  tchnmfval  25558  ioorf  25903  dveflem  26308  tdeglem1  26385  resinf1o  26873  efifo  26884  logcnlem5  26983  resqrtcn  27086  asinf  27209  acosf  27211  atanf  27217  leibpilem2  27278  areaf  27298  emcllem1  27332  igamf  27387  chtf  27444  chpf  27459  ppif  27466  muf  27476  bposlem7  27626  2lgslem1b  27728  pntrf  27899  pntrsumo1  27901  pntsf  27909  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  oldf  28232  newf  28233  leftf  28250  rightf  28251  normf  31734  hosubcli  32380  cnlnadjlem4  32681  cnlnadjlem6  32683  zringfrac  34136  eulerpartlemsf  35041  fiblem  35080  signsvvf  35258  j00smo  35948  derangf  36023  snmlff  36184  ex-sategoelel12  36282  sinccvglem  36527  circum  36529  dnif  37436  bj-evalf  38103  f1omptsnlem  38368  phpreu  38636  poimirlem26  38673  cncfres  38808  lsatset  40156  clsk1independent  45155  lhe4.4ex1a  45422  absfico  46339  clim1fr1  46721  liminfgf  46876  limsup10ex  46891  liminf10ex  46892  dvsinax  47031  wallispilem5  47187  wallispi  47188  stirlinglem5  47196  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  stirlingr  47208  fourierdlem43  47268  fourierdlem57  47281  fourierdlem58  47282  fourierdlem62  47286  fouriersw  47349  0ome  47647  sinnpoly  48049  sprsymrelf  48685  fmtnof1  48728  prmdvdsfmtnof  48779  uspgrsprf  49352  ackendofnn0  49904  dvsec  51039  dvcsc  51040  dvcot  51041