Theorem fvmptg 5758

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃*wmo 2083   ∈ wcel 2205  {copab 4175   ↦ cmpt 4176  ‘cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365

This theorem is referenced by:  fvmpt  5759  fvmpts  5760  fvmpt3  5761  fvmpt2  5766  f1mpt  5950  caofinvl  6301  1stvalg  6349  2ndvalg  6350  brtpos2  6495  rdgon  6630  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  sucinc  6691  sucinc2  6692  omcl  6707  oeicl  6708  oav2  6709  omv2  6711  fvdiagfn  6941  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djulclb  7359  omp1eomlem  7398  ctmlemr  7412  nnnninf  7430  nnnninfeq  7432  cardval3ex  7494  ceilqval  10695  frec2uzzd  10789  frec2uzsucd  10790  monoord2  10875  iseqf1olemqval  10889  iseqf1olemqk  10896  seq3f1olemqsum  10902  seq3f1oleml  10905  seq3f1o  10906  seq3distr  10921  ser3le  10926  hashinfom  11169  hashennn  11171  cjval  11558  reval  11562  imval  11563  cvg1nlemcau  11697  cvg1nlemres  11698  absval  11714  resqrexlemglsq  11735  resqrexlemga  11736  climmpt  12013  climle  12047  climcvg1nlem  12062  summodclem3  12094  summodclem2a  12095  zsumdc  12098  fsum3  12101  fsumcl2lem  12112  sumsnf  12123  isumadd  12145  fsumrev  12157  fsumshft  12158  fsummulc2  12162  iserabs  12189  isumlessdc  12210  divcnv  12211  trireciplem  12214  trirecip  12215  expcnvap0  12216  expcnvre  12217  expcnv  12218  explecnv  12219  geolim  12225  geolim2  12226  geo2lim  12230  geoisum  12231  geoisumr  12232  geoisum1  12233  geoisum1c  12234  cvgratz  12246  mertenslem2  12250  mertensabs  12251  fprodmul  12305  eftvalcn  12371  efval  12375  efcvgfsum  12381  ege2le3  12385  efcj  12387  eftlub  12404  efgt1p2  12409  eflegeo  12415  sinval  12416  cosval  12417  tanvalap  12422  eirraplem  12491  phival  12938  crth  12949  phimullem  12950  ennnfonelemj0  13239  ennnfonelem0  13243  strnfvnd  13319  topnvalg  13551  tgval  13562  2idlval  14779  zrhval  14894  toponsspwpwg  15016  cldval  15093  ntrfval  15094  clsfval  15095  neifval  15134  neival  15137  ismet  15338  isxmet  15339  divcnap  15559  mulc1cncf  15583  depindlem1  16630  djucllem  16711  nnsf  16922  peano3nninf  16924  nninfself  16930  nninfsellemeqinf  16933  dceqnconst  16985  dcapnconst  16986