Theorem fvmptg 5640

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  ∃*wmo 2046   ∈ wcel 2167  {copab 4094   ↦ cmpt 4095  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-iota 5220  df-fun 5261  df-fv 5267

This theorem is referenced by:  fvmpt  5641  fvmpts  5642  fvmpt3  5643  fvmpt2  5648  f1mpt  5821  caofinvl  6165  1stvalg  6209  2ndvalg  6210  brtpos2  6318  rdgon  6453  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  sucinc  6512  sucinc2  6513  omcl  6528  oeicl  6529  oav2  6530  omv2  6532  fvdiagfn  6761  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djulclb  7130  omp1eomlem  7169  ctmlemr  7183  nnnninf  7201  nnnninfeq  7203  cardval3ex  7265  ceilqval  10417  frec2uzzd  10511  frec2uzsucd  10512  monoord2  10597  iseqf1olemqval  10611  iseqf1olemqk  10618  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seq3distr  10643  ser3le  10648  hashinfom  10889  hashennn  10891  cjval  11029  reval  11033  imval  11034  cvg1nlemcau  11168  cvg1nlemres  11169  absval  11185  resqrexlemglsq  11206  resqrexlemga  11207  climmpt  11484  climle  11518  climcvg1nlem  11533  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsum3  11571  fsumcl2lem  11582  sumsnf  11593  isumadd  11615  fsumrev  11627  fsumshft  11628  fsummulc2  11632  iserabs  11659  isumlessdc  11680  divcnv  11681  trireciplem  11684  trirecip  11685  expcnvap0  11686  expcnvre  11687  expcnv  11688  explecnv  11689  geolim  11695  geolim2  11696  geo2lim  11700  geoisum  11701  geoisumr  11702  geoisum1  11703  geoisum1c  11704  cvgratz  11716  mertenslem2  11720  mertensabs  11721  fprodmul  11775  eftvalcn  11841  efval  11845  efcvgfsum  11851  ege2le3  11855  efcj  11857  eftlub  11874  efgt1p2  11879  eflegeo  11885  sinval  11886  cosval  11887  tanvalap  11892  eirraplem  11961  phival  12408  crth  12419  phimullem  12420  ennnfonelemj0  12645  ennnfonelem0  12649  strnfvnd  12725  topnvalg  12955  tgval  12966  2idlval  14136  zrhval  14251  toponsspwpwg  14366  cldval  14443  ntrfval  14444  clsfval  14445  neifval  14484  neival  14487  ismet  14688  isxmet  14689  divcnap  14909  mulc1cncf  14933  djucllem  15554  nnsf  15760  peano3nninf  15762  nninfself  15768  nninfsellemeqinf  15771  dceqnconst  15817  dcapnconst  15818