Theorem fvmptg 5594

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353  ∃*wmo 2027   ∈ wcel 2148  {copab 4065   ↦ cmpt 4066  ‘cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226

This theorem is referenced by:  fvmpt  5595  fvmpts  5596  fvmpt3  5597  fvmpt2  5601  f1mpt  5774  caofinvl  6107  1stvalg  6145  2ndvalg  6146  brtpos2  6254  rdgon  6389  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  sucinc  6448  sucinc2  6449  omcl  6464  oeicl  6465  oav2  6466  omv2  6468  fvdiagfn  6695  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  djulclb  7056  omp1eomlem  7095  ctmlemr  7109  nnnninf  7126  nnnninfeq  7128  cardval3ex  7186  ceilqval  10308  frec2uzzd  10402  frec2uzsucd  10403  monoord2  10479  iseqf1olemqval  10489  iseqf1olemqk  10496  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  seq3distr  10515  ser3le  10520  hashinfom  10760  hashennn  10762  cjval  10856  reval  10860  imval  10861  cvg1nlemcau  10995  cvg1nlemres  10996  absval  11012  resqrexlemglsq  11033  resqrexlemga  11034  climmpt  11310  climle  11344  climcvg1nlem  11359  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsum3  11397  fsumcl2lem  11408  sumsnf  11419  isumadd  11441  fsumrev  11453  fsumshft  11454  fsummulc2  11458  iserabs  11485  isumlessdc  11506  divcnv  11507  trireciplem  11510  trirecip  11511  expcnvap0  11512  expcnvre  11513  expcnv  11514  explecnv  11515  geolim  11521  geolim2  11522  geo2lim  11526  geoisum  11527  geoisumr  11528  geoisum1  11529  geoisum1c  11530  cvgratz  11542  mertenslem2  11546  mertensabs  11547  fprodmul  11601  eftvalcn  11667  efval  11671  efcvgfsum  11677  ege2le3  11681  efcj  11683  eftlub  11700  efgt1p2  11705  eflegeo  11711  sinval  11712  cosval  11713  tanvalap  11718  eirraplem  11786  phival  12215  crth  12226  phimullem  12227  ennnfonelemj0  12404  ennnfonelem0  12408  strnfvnd  12484  topnvalg  12705  tgval  12716  toponsspwpwg  13561  cldval  13638  ntrfval  13639  clsfval  13640  neifval  13679  neival  13682  ismet  13883  isxmet  13884  divcnap  14094  mulc1cncf  14115  djucllem  14591  nnsf  14793  peano3nninf  14795  nninfself  14801  nninfsellemeqinf  14804  dceqnconst  14846  dcapnconst  14847