Theorem fvmptg 5722

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 2231	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2243	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2238	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 2981	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 9	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 4152	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2252	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 5720	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 15	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  ∃*wmo 2080   ∈ wcel 2202  {copab 4149   ↦ cmpt 4150  ‘cfv 5326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334

This theorem is referenced by:  fvmpt  5723  fvmpts  5724  fvmpt3  5725  fvmpt2  5730  f1mpt  5912  caofinvl  6261  1stvalg  6305  2ndvalg  6306  brtpos2  6417  rdgon  6552  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  sucinc  6613  sucinc2  6614  omcl  6629  oeicl  6630  oav2  6631  omv2  6633  fvdiagfn  6862  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djulclb  7254  omp1eomlem  7293  ctmlemr  7307  nnnninf  7325  nnnninfeq  7327  cardval3ex  7389  ceilqval  10569  frec2uzzd  10663  frec2uzsucd  10664  monoord2  10749  iseqf1olemqval  10763  iseqf1olemqk  10770  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seq3distr  10795  ser3le  10800  hashinfom  11041  hashennn  11043  cjval  11407  reval  11411  imval  11412  cvg1nlemcau  11546  cvg1nlemres  11547  absval  11563  resqrexlemglsq  11584  resqrexlemga  11585  climmpt  11862  climle  11896  climcvg1nlem  11911  summodclem3  11943  summodclem2a  11944  zsumdc  11947  fsum3  11950  fsumcl2lem  11961  sumsnf  11972  isumadd  11994  fsumrev  12006  fsumshft  12007  fsummulc2  12011  iserabs  12038  isumlessdc  12059  divcnv  12060  trireciplem  12063  trirecip  12064  expcnvap0  12065  expcnvre  12066  expcnv  12067  explecnv  12068  geolim  12074  geolim2  12075  geo2lim  12079  geoisum  12080  geoisumr  12081  geoisum1  12082  geoisum1c  12083  cvgratz  12095  mertenslem2  12099  mertensabs  12100  fprodmul  12154  eftvalcn  12220  efval  12224  efcvgfsum  12230  ege2le3  12234  efcj  12236  eftlub  12253  efgt1p2  12258  eflegeo  12264  sinval  12265  cosval  12266  tanvalap  12271  eirraplem  12340  phival  12787  crth  12798  phimullem  12799  ennnfonelemj0  13024  ennnfonelem0  13028  strnfvnd  13104  topnvalg  13336  tgval  13347  2idlval  14519  zrhval  14634  toponsspwpwg  14749  cldval  14826  ntrfval  14827  clsfval  14828  neifval  14867  neival  14870  ismet  15071  isxmet  15072  divcnap  15292  mulc1cncf  15316  depindlem1  16346  djucllem  16417  nnsf  16628  peano3nninf  16630  nninfself  16636  nninfsellemeqinf  16639  dceqnconst  16685  dcapnconst  16686