Theorem fvmptd3 5793

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209   ↦ cmpt 4187  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-iota 5332  df-fun 5374  df-fv 5380

This theorem is referenced by:  ofvalg  6302  pw2f1odclem  7124  fival  7294  2omap  7308  inl11  7395  djuss  7400  ctmlemr  7438  ctssdclemn0  7440  ctssdc  7443  enumctlemm  7444  nninfisollemne  7461  nninfisol  7463  fodjum  7476  fodju0  7477  ismkvnex  7485  nninfwlporlemd  7502  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  cc2lem  7622  seqf1oglem2  10935  seqf1og  10936  lswwrd  11329  swrdfv  11403  swrdswrd  11455  xrnegiso  12006  summodclem3  12125  fsumf1o  12135  fsum3ser  12142  fsumadd  12151  sumsnf  12154  prodfdivap  12292  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodf1o  12333  prodsnf  12337  fprodshft  12363  fprodrev  12364  nninfctlemfo  12795  eulerthlemh  12987  eulerthlemth  12988  phisum  12997  1arithlem2  13121  ballotfilemrval  13239  ennnfonelemjn  13271  ennnfonelemp1  13275  ctiunctlemfo  13308  nninfdclemf  13318  nninfdclemp1  13319  ptex  13595  divsfval  13626  divsfvalg  13627  plusffvalg  13659  grpidvalg  13670  issubm  13756  grpinvfvalg  13824  grpinvval  13825  grpsubfvalg  13827  grplactfval  13883  mulgfvalg  13901  issubg  13953  subgex  13956  isnsg  13982  conjghm  14056  conjnmz  14059  qusghm  14062  gzsumconst  14120  gzsummhm2  14123  gzsumshift  14126  gsumsncmn  14133  gsumzfi  14135  gsummhm2fi  14142  prdsplusgfval  14161  prdsmulrfval  14163  prdsinvlem  14173  mgpvalg  14197  srglmhm  14271  srgrmhm  14272  ringlghm  14339  ringrghm  14340  opprvalg  14347  dvdsrvald  14373  isunitd  14386  invrfvald  14402  dvrfvald  14413  issubrng  14480  issubrg  14502  rrgval  14543  rrgsupp  14547  aprval  14564  aprap  14571  aprprop  14574  scaffvalg  14615  lsssetm  14665  lspfval  14697  lspval  14699  sraval  14746  rlmvalg  14763  2idlvalg  14812  expghmap  14914  mulgghm2  14915  mulgrhm  14916  zrhvalg  14925  zrhmulg  14927  zlmval  14934  znval  14943  znzrhval  14954  ntrval  15134  clsval  15135  cnpval  15222  upxp  15296  uptx  15298  txlm  15303  cnmpt11  15307  cnmpt21  15315  ispsmet  15347  mopnval  15466  bdxmet  15525  cncfmptc  15620  cncfmptid  15621  addccncf  15624  negcncf  15629  ivthdec  15668  ivthreinc  15669  hovera  15671  hoverb  15672  hoverlt1  15673  hovergt0  15674  limcmpted  15687  cnmptlimc  15698  dvrecap  15737  dveflem  15750  dvef  15751  plyval  15756  plycoeid3  15781  plyrecj  15787  sgmppw  16020  lgsval  16037  lgsfvalg  16038  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  gausslemma2dlem1f1o  16093  gausslemma2dlem4  16097  lgseisenlem2  16104  2lgslem1b  16122  vtxvalg  16171  iedgvalg  16172  edgvalg  16214  edgopval  16217  edgstruct  16219  vtxdgfifival  16446  wksfval  16477  trlsfvalg  16538  clwwlkg  16548  clwwlknonmpo  16583  eupthsg  16600  depindlem1  16661  pw1map  16939  subctctexmid  16944  nninffeq  16968  nnnninfex  16970  repiecele0  16980  repiecege0  16981  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  iswomni0  17006  dceqnconst  17015  dcapnconst  17016  nconstwlpolemgt0  17019