Theorem fmpti 6291

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ↦ cmpt 4643  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  harf  8348  r0weon  8718  dfac2a  8835  ackbij1lem10  8934  cff  8953  isf32lem9  9066  fin1a2lem2  9106  fin1a2lem4  9108  facmapnn  12934  wwlktovf  13547  cjf  13692  ref  13700  imf  13701  absf  13925  limsupcl  14052  limsupgf  14054  eff  14651  sinf  14693  cosf  14694  bitsf  14987  fnum  15288  fden  15289  prmgapprmo  15604  setcepi  16561  catcfuccl  16582  staffval  18670  ocvfval  19829  pjfval  19869  pjpm  19871  leordtval2  20826  lecldbas  20833  nmfval  22203  nmoffn  22325  nmofval  22328  divcn  22479  xrhmeo  22553  tchex  22824  tchnmfval  22835  ioorf  23147  dveflem  23546  resinf1o  24086  efifo  24097  logcnlem5  24192  resqrtcn  24290  asinf  24399  acosf  24401  atanf  24407  leibpilem2  24468  areaf  24488  emcllem1  24522  igamf  24577  chtf  24634  chpf  24649  ppif  24656  muf  24666  bposlem7  24815  2lgslem1b  24917  pntrf  25052  pntrsumo1  25054  pntsf  25062  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  normf  27364  hosubcli  28012  cnlnadjlem4  28313  cnlnadjlem6  28315  eulerpartlemsf  29748  fiblem  29787  signsvvf  29982  derangf  30404  snmlff  30565  sinccvglem  30820  circum  30822  dnif  31634  f1omptsnlem  32359  phpreu  32563  poimirlem26  32605  cncfres  32734  lsatset  33295  clsk1independent  37364  lhe4.4ex1a  37550  absfico  38405  clim1fr1  38668  dvsinax  38801  wallispilem5  38962  wallispi  38963  stirlinglem5  38971  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  fourierdlem43  39043  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fouriersw  39124  0ome  39419  fmtnof1  39985  prmdvdsfmtnof  40036