Theorem fmpti 6383

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  ∀wral 2912   ↦ cmpt 4729  ⟶wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  harf  8465  r0weon  8835  dfac2a  8952  ackbij1lem10  9051  cff  9070  isf32lem9  9183  fin1a2lem2  9223  fin1a2lem4  9225  facmapnn  13072  wwlktovf  13699  cjf  13844  ref  13852  imf  13853  absf  14077  limsupcl  14204  limsupgf  14206  eff  14812  sinf  14854  cosf  14855  bitsf  15149  fnum  15450  fden  15451  prmgapprmo  15766  setcepi  16738  catcfuccl  16759  staffval  18847  ocvfval  20010  pjfval  20050  pjpm  20052  leordtval2  21016  lecldbas  21023  nmfval  22393  nmoffn  22515  nmofval  22518  divcn  22671  xrhmeo  22745  tchex  23016  tchnmfval  23027  ioorf  23341  dveflem  23742  resinf1o  24282  efifo  24293  logcnlem5  24392  resqrtcn  24490  asinf  24599  acosf  24601  atanf  24607  leibpilem2  24668  areaf  24688  emcllem1  24722  igamf  24777  chtf  24834  chpf  24849  ppif  24856  muf  24866  bposlem7  25015  2lgslem1b  25117  pntrf  25252  pntrsumo1  25254  pntsf  25262  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  normf  27980  hosubcli  28628  cnlnadjlem4  28929  cnlnadjlem6  28931  eulerpartlemsf  30421  fiblem  30460  signsvvf  30656  derangf  31150  snmlff  31311  sinccvglem  31566  circum  31568  dnif  32464  f1omptsnlem  33183  phpreu  33393  poimirlem26  33435  cncfres  33564  lsatset  34277  clsk1independent  38344  lhe4.4ex1a  38528  absfico  39410  clim1fr1  39833  liminfgf  39990  limsup10ex  40005  liminf10ex  40006  dvsinax  40127  wallispilem5  40286  wallispi  40287  stirlinglem5  40295  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  fourierdlem43  40367  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fouriersw  40448  0ome  40743  fmtnof1  41447  prmdvdsfmtnof  41498  sprsymrelf  41745  uspgrsprf  41754