Theorem fvmptg 5725

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  ∃*wmo 2079   ∈ wcel 2201  {copab 4150   ↦ cmpt 4151  ‘cfv 5328

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 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-iota 5288  df-fun 5330  df-fv 5336

This theorem is referenced by:  fvmpt  5726  fvmpts  5727  fvmpt3  5728  fvmpt2  5733  f1mpt  5917  caofinvl  6266  1stvalg  6310  2ndvalg  6311  brtpos2  6422  rdgon  6557  frec0g  6568  freccllem  6573  frecfcllem  6575  frecsuclem  6577  sucinc  6618  sucinc2  6619  omcl  6634  oeicl  6635  oav2  6636  omv2  6638  fvdiagfn  6867  djulclr  7253  djurclr  7254  djulcl  7255  djurcl  7256  djulclb  7259  omp1eomlem  7298  ctmlemr  7312  nnnninf  7330  nnnninfeq  7332  cardval3ex  7394  ceilqval  10574  frec2uzzd  10668  frec2uzsucd  10669  monoord2  10754  iseqf1olemqval  10768  iseqf1olemqk  10775  seq3f1olemqsum  10781  seq3f1oleml  10784  seq3f1o  10785  seq3distr  10800  ser3le  10805  hashinfom  11046  hashennn  11048  cjval  11428  reval  11432  imval  11433  cvg1nlemcau  11567  cvg1nlemres  11568  absval  11584  resqrexlemglsq  11605  resqrexlemga  11606  climmpt  11883  climle  11917  climcvg1nlem  11932  summodclem3  11964  summodclem2a  11965  zsumdc  11968  fsum3  11971  fsumcl2lem  11982  sumsnf  11993  isumadd  12015  fsumrev  12027  fsumshft  12028  fsummulc2  12032  iserabs  12059  isumlessdc  12080  divcnv  12081  trireciplem  12084  trirecip  12085  expcnvap0  12086  expcnvre  12087  expcnv  12088  explecnv  12089  geolim  12095  geolim2  12096  geo2lim  12100  geoisum  12101  geoisumr  12102  geoisum1  12103  geoisum1c  12104  cvgratz  12116  mertenslem2  12120  mertensabs  12121  fprodmul  12175  eftvalcn  12241  efval  12245  efcvgfsum  12251  ege2le3  12255  efcj  12257  eftlub  12274  efgt1p2  12279  eflegeo  12285  sinval  12286  cosval  12287  tanvalap  12292  eirraplem  12361  phival  12808  crth  12819  phimullem  12820  ennnfonelemj0  13045  ennnfonelem0  13049  strnfvnd  13125  topnvalg  13357  tgval  13368  2idlval  14540  zrhval  14655  toponsspwpwg  14775  cldval  14852  ntrfval  14853  clsfval  14854  neifval  14893  neival  14896  ismet  15097  isxmet  15098  divcnap  15318  mulc1cncf  15342  depindlem1  16386  djucllem  16457  nnsf  16670  peano3nninf  16672  nninfself  16678  nninfsellemeqinf  16681  dceqnconst  16732  dcapnconst  16733