Theorem fvmptg 6994

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 2766	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2777	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2770	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3673	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5198	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2789	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6992	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 21	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃*wmo 2568  {copab 5178   ↦ cmpt 5197  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551

This theorem is used by:  fvmpti  6995  fvmpt  6996  fvmpt2f  6997  fvtresfn  6999  fvmpts  7000  fvmpt3  7001  fvmptd3  7020  fvmptss2  7023  f1mpt  7266  bropfvvvv  8096  tz7.44-3  8404  pw2f1olem  9079  wdom2d  9552  tz9.12lem3  9771  djurcl  9916  djur  9924  djuun  9931  cardval3  9957  cfval  10248  coftr  10275  fin1a2lem1  10402  fin1a2lem12  10413  axdc2lem  10450  pwcfsdom  10586  tskmval  10842  lsw  14621  swrdswrd  14766  trclfv  15063  relexpsucnnr  15088  dfrtrclrec2  15121  rtrclreclem2  15122  summolem2a  15792  prodmolem2a  16014  divsfval  17626  joinfval  18452  meetfval  18466  symgextfv  19519  symgextfve  19520  pmtrdifwrdel2lem1  19585  efgtf  19823  rrgsupp  20837  uvcvval  21973  ply1sclid  22486  submaval0  22774  m2detleiblem3  22823  m2detleiblem4  22824  maduval  22832  minmar1val0  22841  toponsspwpw  23116  cldval  23217  ntrfval  23218  clsfval  23219  opncldf3  23280  neifval  23293  lpfval  23332  islocfin  23711  kqfval  23917  stdbdxmet  24709  cmetcaulem  25484  bcth3  25527  itg2gt0  25956  ellimc2  26073  coe1termlem  26452  bdayval  27849  oldval  28064  clwlkclwwlkfo  30397  grpoinvfval  30911  grpodivfval  30923  nlfnval  32270  sigaval  34532  measval  34620  measdivcst  34646  measdivcstALTV  34647  probfinmeasbALTV  34851  ptpconn  35746  cvmsval  35779  ex-sategoelel12  35940  imageval  36441  fvimage  36442  tailfval  36924  tailval  36925  curfv  38292  heiborlem4  38506  lkrval  39903  cdleme31fv  41205  docavalN  41938  dochval  42166  mapdval  42443  hvmapval  42575  hvmapvalvalN  42576  hdmap1vallem  42612  hdmapval  42643  hgmapval  42702  mzpval  43504  mzpsubst  43520  pw2f1o2val  43807  refsum2cnlem1  45798  stoweidlem26  46781  stirlinglem8  46836  fourierdlem50  46911  caragenval  47248  fargshiftfv  48229  lincvalsc0  49242  linc0scn0  49244  linc1  49246  lincscm  49251  crosspv1i  50683  crosspv2i  50684  crosspv3i  50685  crosspdot0i  50686