Theorem fvmptd3 5802

Description: Deduction version of fvmpt 5785. (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 5801	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 415	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209   ↦ cmpt 4193  ‘cfv 5380

This proof depends on 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 4251  ax-pow 4313  ax-pr 4348

This proof 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 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388

This theorem is used by:  ofvalg  6316  pw2f1odclem  7138  fival  7309  2omap  7324  inl11  7411  djuss  7416  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  nninfisollemne  7477  nninfisol  7479  fodjum  7492  fodju0  7493  ismkvnex  7501  nninfwlporlemd  7518  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  cc2lem  7638  indv  9304  seqf1oglem2  10978  seqf1og  10979  lswwrd  11373  swrdfv  11447  swrdswrd  11499  xrnegiso  12053  summodclem3  12172  fsumf1o  12182  fsum3ser  12189  fsumadd  12198  sumsnf  12201  prodfdivap  12339  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodf1o  12380  prodsnf  12384  fprodshft  12410  fprodrev  12411  nninfctlemfo  12842  eulerthlemh  13038  eulerthlemth  13039  phisum  13048  1arithlem2  13172  ballotfilemrval  13319  ennnfonelemjn  13351  ennnfonelemp1  13355  ctiunctlemfo  13388  nninfdclemf  13398  nninfdclemp1  13399  ptex  13677  divsfval  13708  divsfvalg  13709  plusffvalg  13741  grpidvalg  13752  issubm  13838  grpinvfvalg  13906  grpinvval  13907  grpsubfvalg  13909  grplactfval  13965  mulgfvalg  13983  issubg  14035  subgex  14038  isnsg  14064  conjghm  14138  conjnmz  14141  qusghm  14144  cntzex  14150  cntrval  14151  cntzfval  14152  gzsumconst  14233  gzsummhm2  14236  gzsumshift  14239  gsumsncmn  14246  gsumzfi  14248  gsummhm2fi  14265  gsum2dfi  14273  prdsplusgfval  14291  prdsmulrfval  14293  prdsinvlem  14303  mgpvalg  14327  srglmhm  14404  srgrmhm  14405  ringlghm  14473  ringrghm  14474  opprvalg  14483  dvdsrvald  14509  isunitd  14522  invrfvald  14538  dvrfvald  14549  issubrng  14616  issubrg  14638  rrgval  14679  rrgsupp  14683  aprval  14700  aprap  14707  aprprop  14710  scaffvalg  14752  lsssetm  14802  lspfval  14834  lspval  14836  sraval  14883  rlmvalg  14900  2idlvalg  14949  expghmap  15051  mulgghm2  15052  mulgrhm  15053  zrhvalg  15062  zrhmulg  15064  zlmval  15071  znval  15080  znzrhval  15091  aspval  15124  asclfval  15130  asclvald  15131  psrlidmfi  15199  psrridmfi  15200  ntrval  15336  clsval  15337  cnpval  15424  upxp  15498  uptx  15500  txlm  15505  cnmpt11  15509  cnmpt21  15517  ispsmet  15549  mopnval  15668  bdxmet  15727  cncfmptc  15822  cncfmptid  15823  addccncf  15826  negcncf  15831  ivthdec  15870  ivthreinc  15871  hovera  15873  hoverb  15874  hoverlt1  15875  hovergt0  15876  limcmpted  15889  cnmptlimc  15900  dvrecap  15939  dveflem  15952  dvef  15953  plyval  15958  plycoeid3  15983  plyrecj  15989  log2tlbndlog2  16220  chtqcl  16244  chtqval  16245  ppiqval  16248  prmorcht  16282  sgmppw  16286  bposlem5  16315  bposlem7  16317  bposlem9  16319  lgsval  16328  lgsfvalg  16329  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  gausslemma2dlem1f1o  16384  gausslemma2dlem4  16388  lgseisenlem2  16395  2lgslem1b  16413  vtxvalg  16462  iedgvalg  16463  edgvalg  16505  edgopval  16508  edgstruct  16510  vtxdgfifival  16737  wksfval  16768  trlsfvalg  16829  clwwlkg  16839  clwwlknonmpo  16874  eupthsg  16891  depindlem1  16952  pw1map  17230  subctctexmid  17235  nninffeq  17269  nnnninfex  17271  repiecele0  17281  repiecege0  17282  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  iswomni0  17308  dceqnconst  17317  dcapnconst  17318  nconstwlpolemgt0  17321