Theorem fvmptg 6939

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 2737	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2748	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2741	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3654	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5168	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2760	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6937	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 20	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃*wmo 2538  {copab 5148   ↦ cmpt 5167  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmpti  6940  fvmpt  6941  fvmpt2f  6942  fvtresfn  6944  fvmpts  6945  fvmpt3  6946  fvmptd3  6965  fvmptss2  6968  f1mpt  7209  bropfvvvv  8035  tz7.44-3  8340  pw2f1olem  9012  wdom2d  9488  tz9.12lem3  9704  djurcl  9826  djur  9834  djuun  9841  cardval3  9867  cfval  10160  coftr  10186  fin1a2lem1  10313  fin1a2lem12  10324  axdc2lem  10361  pwcfsdom  10497  tskmval  10753  lsw  14517  swrdswrd  14658  trclfv  14953  relexpsucnnr  14978  dfrtrclrec2  15011  rtrclreclem2  15012  summolem2a  15668  prodmolem2a  15890  divsfval  17502  joinfval  18328  meetfval  18342  symgextfv  19384  symgextfve  19385  pmtrdifwrdel2lem1  19450  efgtf  19688  rrgsupp  20669  uvcvval  21776  ply1sclid  22263  submaval0  22555  m2detleiblem3  22604  m2detleiblem4  22605  maduval  22613  minmar1val0  22622  toponsspwpw  22897  cldval  22998  ntrfval  22999  clsfval  23000  opncldf3  23061  neifval  23074  lpfval  23113  islocfin  23492  kqfval  23698  stdbdxmet  24490  cmetcaulem  25265  bcth3  25308  itg2gt0  25737  ellimc2  25854  coe1termlem  26233  bdayval  27626  oldval  27840  clwlkclwwlkfo  30094  grpoinvfval  30608  grpodivfval  30620  nlfnval  31967  sigaval  34271  measval  34358  measdivcst  34384  measdivcstALTV  34385  probfinmeasbALTV  34589  ptpconn  35431  cvmsval  35464  ex-sategoelel12  35625  imageval  36126  fvimage  36127  tailfval  36570  tailval  36571  curfv  37935  heiborlem4  38149  lkrval  39548  cdleme31fv  40850  docavalN  41583  dochval  41811  mapdval  42088  hvmapval  42220  hvmapvalvalN  42221  hdmap1vallem  42257  hdmapval  42288  hgmapval  42347  mzpval  43178  mzpsubst  43194  pw2f1o2val  43485  refsum2cnlem1  45486  stoweidlem26  46472  stirlinglem8  46527  fourierdlem50  46602  caragenval  46939  nthrucw  47332  fargshiftfv  47911  lincvalsc0  48909  linc0scn0  48911  linc1  48913  lincscm  48918