Theorem fvmptg 5718

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

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

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332

This theorem is referenced by:  fvmpt  5719  fvmpts  5720  fvmpt3  5721  fvmpt2  5726  f1mpt  5907  caofinvl  6256  1stvalg  6300  2ndvalg  6301  brtpos2  6412  rdgon  6547  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  sucinc  6608  sucinc2  6609  omcl  6624  oeicl  6625  oav2  6626  omv2  6628  fvdiagfn  6857  djulclr  7242  djurclr  7243  djulcl  7244  djurcl  7245  djulclb  7248  omp1eomlem  7287  ctmlemr  7301  nnnninf  7319  nnnninfeq  7321  cardval3ex  7383  ceilqval  10561  frec2uzzd  10655  frec2uzsucd  10656  monoord2  10741  iseqf1olemqval  10755  iseqf1olemqk  10762  seq3f1olemqsum  10768  seq3f1oleml  10771  seq3f1o  10772  seq3distr  10787  ser3le  10792  hashinfom  11033  hashennn  11035  cjval  11399  reval  11403  imval  11404  cvg1nlemcau  11538  cvg1nlemres  11539  absval  11555  resqrexlemglsq  11576  resqrexlemga  11577  climmpt  11854  climle  11888  climcvg1nlem  11903  summodclem3  11934  summodclem2a  11935  zsumdc  11938  fsum3  11941  fsumcl2lem  11952  sumsnf  11963  isumadd  11985  fsumrev  11997  fsumshft  11998  fsummulc2  12002  iserabs  12029  isumlessdc  12050  divcnv  12051  trireciplem  12054  trirecip  12055  expcnvap0  12056  expcnvre  12057  expcnv  12058  explecnv  12059  geolim  12065  geolim2  12066  geo2lim  12070  geoisum  12071  geoisumr  12072  geoisum1  12073  geoisum1c  12074  cvgratz  12086  mertenslem2  12090  mertensabs  12091  fprodmul  12145  eftvalcn  12211  efval  12215  efcvgfsum  12221  ege2le3  12225  efcj  12227  eftlub  12244  efgt1p2  12249  eflegeo  12255  sinval  12256  cosval  12257  tanvalap  12262  eirraplem  12331  phival  12778  crth  12789  phimullem  12790  ennnfonelemj0  13015  ennnfonelem0  13019  strnfvnd  13095  topnvalg  13327  tgval  13338  2idlval  14509  zrhval  14624  toponsspwpwg  14739  cldval  14816  ntrfval  14817  clsfval  14818  neifval  14857  neival  14860  ismet  15061  isxmet  15062  divcnap  15282  mulc1cncf  15306  djucllem  16346  nnsf  16557  peano3nninf  16559  nninfself  16565  nninfsellemeqinf  16568  dceqnconst  16614  dcapnconst  16615