Theorem fvmptg 6989

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.

Step	Hyp	Ref	Expression
1		eqid 2763	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2774	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2767	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3671	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5194	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2786	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6987	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 21	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃*wmo 2565  {copab 5174   ↦ cmpt 5193  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  fvmpti  6990  fvmpt  6991  fvmpt2f  6992  fvtresfn  6994  fvmpts  6995  fvmpt3  6996  fvmptd3  7015  fvmptss2  7018  f1mpt  7261  bropfvvvv  8088  tz7.44-3  8396  pw2f1olem  9070  wdom2d  9543  tz9.12lem3  9762  djurcl  9898  djur  9906  djuun  9913  cardval3  9939  cfval  10231  coftr  10258  fin1a2lem1  10385  fin1a2lem12  10396  axdc2lem  10433  pwcfsdom  10569  tskmval  10825  lsw  14603  swrdswrd  14744  trclfv  15039  relexpsucnnr  15064  dfrtrclrec2  15097  rtrclreclem2  15098  summolem2a  15768  prodmolem2a  15990  divsfval  17602  joinfval  18428  meetfval  18442  symgextfv  19489  symgextfve  19490  pmtrdifwrdel2lem1  19555  efgtf  19793  rrgsupp  20787  uvcvval  21917  ply1sclid  22430  submaval0  22718  m2detleiblem3  22767  m2detleiblem4  22768  maduval  22776  minmar1val0  22785  toponsspwpw  23060  cldval  23161  ntrfval  23162  clsfval  23163  opncldf3  23224  neifval  23237  lpfval  23276  islocfin  23655  kqfval  23861  stdbdxmet  24653  cmetcaulem  25428  bcth3  25471  itg2gt0  25900  ellimc2  26017  coe1termlem  26396  bdayval  27790  oldval  28005  clwlkclwwlkfo  30338  grpoinvfval  30852  grpodivfval  30864  nlfnval  32211  sigaval  34479  measval  34566  measdivcst  34592  measdivcstALTV  34593  probfinmeasbALTV  34797  ptpconn  35703  cvmsval  35736  ex-sategoelel12  35897  imageval  36398  fvimage  36399  tailfval  36861  tailval  36862  curfv  38229  heiborlem4  38443  lkrval  39840  cdleme31fv  41142  docavalN  41875  dochval  42103  mapdval  42380  hvmapval  42512  hvmapvalvalN  42513  hdmap1vallem  42549  hdmapval  42580  hgmapval  42639  mzpval  43443  mzpsubst  43459  pw2f1o2val  43746  refsum2cnlem1  45737  stoweidlem26  46720  stirlinglem8  46775  fourierdlem50  46850  caragenval  47187  nthrucw  47582  fargshiftfv  48165  lincvalsc0  49178  linc0scn0  49180  linc1  49182  lincscm  49187