ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fvmptg GIF version

Theorem fvmptg 5465
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 2117 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2129 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2124 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 2832 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 9 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 3961 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2138 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 5463 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 15 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1316  wcel 1465  ∃*wmo 1978  {copab 3958  cmpt 3959  cfv 5093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-sbc 2883  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-mpt 3961  df-id 4185  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-iota 5058  df-fun 5095  df-fv 5101
This theorem is referenced by:  fvmpt  5466  fvmpts  5467  fvmpt3  5468  fvmpt2  5472  f1mpt  5640  caofinvl  5972  1stvalg  6008  2ndvalg  6009  brtpos2  6116  rdgon  6251  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  sucinc  6309  sucinc2  6310  omcl  6325  oeicl  6326  oav2  6327  omv2  6329  fvdiagfn  6555  djulclr  6902  djurclr  6903  djulcl  6904  djurcl  6905  djulclb  6908  omp1eomlem  6947  ctmlemr  6961  nnnninf  6991  cardval3ex  7009  ceilqval  10047  frec2uzzd  10141  frec2uzsucd  10142  monoord2  10218  iseqf1olemqval  10228  iseqf1olemqk  10235  seq3f1olemqsum  10241  seq3f1oleml  10244  seq3f1o  10245  seq3distr  10254  ser3le  10259  hashinfom  10492  hashennn  10494  cjval  10585  reval  10589  imval  10590  cvg1nlemcau  10724  cvg1nlemres  10725  absval  10741  resqrexlemglsq  10762  resqrexlemga  10763  climmpt  11037  climle  11071  climcvg1nlem  11086  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsum3  11124  fsumcl2lem  11135  sumsnf  11146  isumadd  11168  fsumrev  11180  fsumshft  11181  fsummulc2  11185  iserabs  11212  isumlessdc  11233  divcnv  11234  trireciplem  11237  trirecip  11238  expcnvap0  11239  expcnvre  11240  expcnv  11241  explecnv  11242  geolim  11248  geolim2  11249  geo2lim  11253  geoisum  11254  geoisumr  11255  geoisum1  11256  geoisum1c  11257  cvgratz  11269  mertenslem2  11273  mertensabs  11274  eftvalcn  11290  efval  11294  efcvgfsum  11300  ege2le3  11304  efcj  11306  eftlub  11323  efgt1p2  11328  eflegeo  11335  sinval  11336  cosval  11337  tanvalap  11342  eirraplem  11410  phival  11816  crth  11827  phimullem  11828  ennnfonelemj0  11841  ennnfonelem0  11845  strnfvnd  11906  topnvalg  12059  toponsspwpwg  12116  tgval  12145  cldval  12195  ntrfval  12196  clsfval  12197  neifval  12236  neival  12239  ismet  12440  isxmet  12441  divcnap  12651  mulc1cncf  12672  djucllem  12934  nnsf  13126  peano3nninf  13128  nninfalllemn  13129  nninfself  13136  nninfsellemeqinf  13139
  Copyright terms: Public domain W3C validator