Theorem fvmptg 6766

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃*wmo 2620  {copab 5128   ↦ cmpt 5146  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363

This theorem is referenced by:  fvmpti  6767  fvmpt  6768  fvmpt2f  6769  fvtresfn  6770  fvmpts  6771  fvmpt3  6772  fvmptd3  6791  fvmptss2  6793  f1mpt  7019  bropfvvvv  7787  tz7.44-3  8044  pw2f1olem  8621  wdom2d  9044  tz9.12lem3  9218  djurcl  9340  djur  9348  djuun  9355  cardval3  9381  cfval  9669  coftr  9695  fin1a2lem1  9822  fin1a2lem12  9833  axdc2lem  9870  pwcfsdom  10005  tskmval  10261  lsw  13916  swrdswrd  14067  trclfv  14360  relexpsucnnr  14384  dfrtrclrec2  14416  rtrclreclem1  14417  summolem2a  15072  prodmolem2a  15288  divsfval  16820  joinfval  17611  meetfval  17625  symgextfv  18546  symgextfve  18547  pmtrdifwrdel2lem1  18612  efgtf  18848  rrgsupp  20064  ply1sclid  20456  uvcvval  20930  submaval0  21189  m2detleiblem3  21238  m2detleiblem4  21239  maduval  21247  minmar1val0  21256  toponsspwpw  21530  cldval  21631  ntrfval  21632  clsfval  21633  opncldf3  21694  neifval  21707  lpfval  21746  islocfin  22125  kqfval  22331  stdbdxmet  23125  cmetcaulem  23891  bcth3  23934  itg2gt0  24361  ellimc2  24475  coe1termlem  24848  clwlkclwwlkfo  27787  grpoinvfval  28299  grpodivfval  28311  nlfnval  29658  sigaval  31370  measval  31457  measdivcst  31483  measdivcstALTV  31484  probfinmeasbALTV  31687  ptpconn  32480  cvmsval  32513  ex-sategoelel12  32674  bdayval  33155  imageval  33391  fvimage  33392  tailfval  33720  tailval  33721  curfv  34887  heiborlem4  35107  lkrval  36239  cdleme31fv  37541  docavalN  38274  dochval  38502  mapdval  38779  hvmapval  38911  hvmapvalvalN  38912  hdmap1vallem  38948  hdmapval  38979  hgmapval  39038  mzpval  39378  mzpsubst  39394  pw2f1o2val  39685  refsum2cnlem1  41343  stoweidlem26  42360  stirlinglem8  42415  fourierdlem50  42490  caragenval  42824  fargshiftfv  43648  lincvalsc0  44525  linc0scn0  44527  linc1  44529  lincscm  44534