Theorem fvmptg 5715

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  ∃*wmo 2078   ∈ wcel 2200  {copab 4144   ↦ cmpt 4145  ‘cfv 5321

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-iota 5281  df-fun 5323  df-fv 5329

This theorem is referenced by:  fvmpt  5716  fvmpts  5717  fvmpt3  5718  fvmpt2  5723  f1mpt  5904  caofinvl  6253  1stvalg  6297  2ndvalg  6298  brtpos2  6408  rdgon  6543  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  sucinc  6604  sucinc2  6605  omcl  6620  oeicl  6621  oav2  6622  omv2  6624  fvdiagfn  6853  djulclr  7232  djurclr  7233  djulcl  7234  djurcl  7235  djulclb  7238  omp1eomlem  7277  ctmlemr  7291  nnnninf  7309  nnnninfeq  7311  cardval3ex  7373  ceilqval  10545  frec2uzzd  10639  frec2uzsucd  10640  monoord2  10725  iseqf1olemqval  10739  iseqf1olemqk  10746  seq3f1olemqsum  10752  seq3f1oleml  10755  seq3f1o  10756  seq3distr  10771  ser3le  10776  hashinfom  11017  hashennn  11019  cjval  11377  reval  11381  imval  11382  cvg1nlemcau  11516  cvg1nlemres  11517  absval  11533  resqrexlemglsq  11554  resqrexlemga  11555  climmpt  11832  climle  11866  climcvg1nlem  11881  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsum3  11919  fsumcl2lem  11930  sumsnf  11941  isumadd  11963  fsumrev  11975  fsumshft  11976  fsummulc2  11980  iserabs  12007  isumlessdc  12028  divcnv  12029  trireciplem  12032  trirecip  12033  expcnvap0  12034  expcnvre  12035  expcnv  12036  explecnv  12037  geolim  12043  geolim2  12044  geo2lim  12048  geoisum  12049  geoisumr  12050  geoisum1  12051  geoisum1c  12052  cvgratz  12064  mertenslem2  12068  mertensabs  12069  fprodmul  12123  eftvalcn  12189  efval  12193  efcvgfsum  12199  ege2le3  12203  efcj  12205  eftlub  12222  efgt1p2  12227  eflegeo  12233  sinval  12234  cosval  12235  tanvalap  12240  eirraplem  12309  phival  12756  crth  12767  phimullem  12768  ennnfonelemj0  12993  ennnfonelem0  12997  strnfvnd  13073  topnvalg  13305  tgval  13316  2idlval  14487  zrhval  14602  toponsspwpwg  14717  cldval  14794  ntrfval  14795  clsfval  14796  neifval  14835  neival  14838  ismet  15039  isxmet  15040  divcnap  15260  mulc1cncf  15284  djucllem  16273  nnsf  16485  peano3nninf  16487  nninfself  16493  nninfsellemeqinf  16496  dceqnconst  16542  dcapnconst  16543