Theorem fvmptd3 5730

Description: Deduction version of fvmpt 5713. (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 2372	. . 3 ⊢ Ⅎ𝑥𝐴
4		nfcv 2372	. . 3 ⊢ Ⅎ𝑥𝐶
5		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
6		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
7	3, 4, 5, 6	fvmptf 5729	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 411	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200   ↦ cmpt 4145  ‘cfv 5318

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 4258  ax-pr 4293

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-csb 3125  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 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326

This theorem is referenced by:  ofvalg  6234  pw2f1odclem  7003  fival  7148  inl11  7243  djuss  7248  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  nninfisollemne  7309  nninfisol  7311  fodjum  7324  fodju0  7325  ismkvnex  7333  nninfwlporlemd  7350  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  cc2lem  7463  seqf1oglem2  10754  seqf1og  10755  lswwrd  11131  swrdfv  11200  swrdswrd  11252  xrnegiso  11788  summodclem3  11906  fsumf1o  11916  fsum3ser  11923  fsumadd  11932  sumsnf  11935  prodfdivap  12073  prodmodclem3  12101  prodmodclem2a  12102  fprodseq  12109  fprodf1o  12114  prodsnf  12118  fprodshft  12144  fprodrev  12145  nninfctlemfo  12576  eulerthlemh  12768  eulerthlemth  12769  phisum  12778  1arithlem2  12902  ennnfonelemjn  12988  ennnfonelemp1  12992  ctiunctlemfo  13025  nninfdclemf  13035  nninfdclemp1  13036  ptex  13312  prdsplusgfval  13332  prdsmulrfval  13334  divsfval  13376  divsfvalg  13377  plusffvalg  13410  grpidvalg  13421  issubm  13520  gsumfzz  13543  grpinvfvalg  13590  grpinvval  13591  grpsubfvalg  13593  grplactfval  13649  prdsinvlem  13656  mulgfvalg  13673  issubg  13725  subgex  13728  isnsg  13754  conjghm  13828  conjnmz  13831  qusghm  13834  gsumfzconst  13893  gsumfzmhm2  13896  mgpvalg  13901  srglmhm  13971  srgrmhm  13972  ringlghm  14039  ringrghm  14040  opprvalg  14047  dvdsrvald  14072  isunitd  14085  invrfvald  14101  dvrfvald  14112  issubrng  14178  issubrg  14200  rrgval  14241  aprval  14261  aprap  14265  scaffvalg  14285  lsssetm  14335  lspfval  14367  lspval  14369  sraval  14416  rlmvalg  14433  2idlvalg  14482  expghmap  14586  mulgghm2  14587  mulgrhm  14588  zrhvalg  14597  zrhmulg  14599  zlmval  14606  znval  14615  znzrhval  14626  ntrval  14799  clsval  14800  cnpval  14887  upxp  14961  uptx  14963  txlm  14968  cnmpt11  14972  cnmpt21  14980  ispsmet  15012  mopnval  15131  bdxmet  15190  cncfmptc  15285  cncfmptid  15286  addccncf  15289  negcncf  15294  ivthdec  15333  ivthreinc  15334  hovera  15336  hoverb  15337  hoverlt1  15338  hovergt0  15339  limcmpted  15352  cnmptlimc  15363  dvrecap  15402  dveflem  15415  dvef  15416  plyval  15421  plycoeid3  15446  plyrecj  15452  sgmppw  15681  lgsval  15698  lgsfvalg  15699  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  gausslemma2dlem1f1o  15754  gausslemma2dlem4  15758  lgseisenlem2  15765  2lgslem1b  15783  vtxvalg  15832  iedgvalg  15833  edgvalg  15875  edgopval  15877  edgstruct  15879  vtxdgfifival  16050  wksfval  16063  trlsfvalg  16122  clwwlkg  16131  2omap  16418  pw1map  16420  subctctexmid  16425  nninffeq  16446  nnnninfex  16448  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  iswomni0  16479  dceqnconst  16488  dcapnconst  16489  nconstwlpolemgt0  16492