MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptg Structured version   Visualization version   GIF version

Theorem fvmptg 6763
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptg.1 (𝑥 = 𝐴𝐵 = 𝐶)
fvmptg.2 𝐹 = (𝑥𝐷𝐵)
Assertion
Ref Expression
fvmptg ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝐹(𝑥)

Proof of Theorem fvmptg
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqid 2826 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2837 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2830 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3702 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 5144 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2849 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6761 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  ∃*wmo 2618  {copab 5125  cmpt 5143  cfv 6352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6312  df-fun 6354  df-fv 6360
This theorem is referenced by:  fvmpti  6764  fvmpt  6765  fvmpt2f  6766  fvtresfn  6767  fvmpts  6768  fvmpt3  6769  fvmptd3  6787  fvmptss2  6789  f1mpt  7013  bropfvvvv  7778  tz7.44-3  8035  pw2f1olem  8610  wdom2d  9033  tz9.12lem3  9207  djurcl  9329  djur  9337  djuun  9344  cardval3  9370  cfval  9658  coftr  9684  fin1a2lem1  9811  fin1a2lem12  9822  axdc2lem  9859  pwcfsdom  9994  tskmval  10250  lsw  13906  swrdswrd  14057  trclfv  14350  relexpsucnnr  14374  dfrtrclrec2  14406  rtrclreclem1  14407  summolem2a  15062  prodmolem2a  15278  divsfval  16810  joinfval  17601  meetfval  17615  symgextfv  18466  symgextfve  18467  pmtrdifwrdel2lem1  18532  efgtf  18768  rrgsupp  19983  ply1sclid  20373  uvcvval  20846  submaval0  21105  m2detleiblem3  21154  m2detleiblem4  21155  maduval  21163  minmar1val0  21172  toponsspwpw  21446  cldval  21547  ntrfval  21548  clsfval  21549  opncldf3  21610  neifval  21623  lpfval  21662  islocfin  22041  kqfval  22247  stdbdxmet  23040  cmetcaulem  23806  bcth3  23849  itg2gt0  24276  ellimc2  24390  coe1termlem  24763  clwlkclwwlkfo  27701  grpoinvfval  28213  grpodivfval  28225  nlfnval  29572  sigaval  31256  measval  31343  measdivcst  31369  measdivcstALTV  31370  probfinmeasbALTV  31573  ptpconn  32364  cvmsval  32397  ex-sategoelel12  32558  bdayval  33039  imageval  33275  fvimage  33276  tailfval  33604  tailval  33605  curfv  34739  heiborlem4  34960  lkrval  36091  cdleme31fv  37393  docavalN  38126  dochval  38354  mapdval  38631  hvmapval  38763  hvmapvalvalN  38764  hdmap1vallem  38800  hdmapval  38831  hgmapval  38890  mzpval  39194  mzpsubst  39210  pw2f1o2val  39501  refsum2cnlem1  41159  stoweidlem26  42177  stirlinglem8  42232  fourierdlem50  42307  caragenval  42641  fargshiftfv  43431  lincvalsc0  44308  linc0scn0  44310  linc1  44312  lincscm  44317
  Copyright terms: Public domain W3C validator