Theorem fvmptd3 5611

Description: Deduction version of fvmpt 5595. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
fvmptd3.1	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmptd3.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptd3.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd3.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd3	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd3

Step	Hyp	Ref	Expression
1		fvmptd3.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
2		fvmptd3.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		nfcv 2319	. . 3 ⊢ Ⅎ𝑥𝐴
4		nfcv 2319	. . 3 ⊢ Ⅎ𝑥𝐶
5		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
6		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
7	3, 4, 5, 6	fvmptf 5610	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 411	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148   ↦ 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-csb 3060  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:  ofvalg  6094  fival  6971  inl11  7066  djuss  7071  ctmlemr  7109  ctssdclemn0  7111  ctssdc  7114  enumctlemm  7115  nninfisollemne  7131  nninfisol  7133  fodjum  7146  fodju0  7147  ismkvnex  7155  nninfwlporlemd  7172  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  cc2lem  7267  xrnegiso  11272  summodclem3  11390  fsumf1o  11400  fsum3ser  11407  fsumadd  11416  sumsnf  11419  prodfdivap  11557  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  fprodf1o  11598  prodsnf  11602  fprodshft  11628  fprodrev  11629  eulerthlemh  12233  eulerthlemth  12234  phisum  12242  1arithlem2  12364  ennnfonelemjn  12405  ennnfonelemp1  12409  ctiunctlemfo  12442  nninfdclemf  12452  nninfdclemp1  12453  ptex  12718  divsfvalg  12753  plusffvalg  12786  grpidvalg  12797  issubm  12868  grpinvfvalg  12920  grpinvval  12921  grpsubfvalg  12923  grplactfval  12976  mulgfvalg  12990  issubg  13038  subgex  13041  isnsg  13067  mgpvalg  13138  srglmhm  13181  srgrmhm  13182  opprvalg  13246  reldvdsrsrg  13266  dvdsrvald  13267  isunitd  13280  invrfvald  13296  dvrfvald  13307  issubrg  13347  aprval  13377  aprap  13381  scaffvalg  13401  lsssetm  13449  ntrval  13649  clsval  13650  cnpval  13737  upxp  13811  uptx  13813  txlm  13818  cnmpt11  13822  cnmpt21  13830  ispsmet  13862  mopnval  13981  bdxmet  14040  cncfmptc  14121  cncfmptid  14122  addccncf  14125  negcncf  14127  ivthdec  14161  limcmpted  14171  cnmptlimc  14182  dvrecap  14216  dveflem  14226  dvef  14227  lgsval  14444  lgsfvalg  14445  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgseisenlem2  14490  subctctexmid  14789  nninffeq  14808  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  iswomni0  14838  dceqnconst  14847  dcapnconst  14848  nconstwlpolemgt0  14851