Theorem fvmptd3 5799

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

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

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 4249  ax-pow 4311  ax-pr 4346

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 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385

This theorem is used by:  ofvalg  6312  pw2f1odclem  7134  fival  7304  2omap  7319  inl11  7406  djuss  7411  ctmlemr  7449  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  nninfisollemne  7472  nninfisol  7474  fodjum  7487  fodju0  7488  ismkvnex  7496  nninfwlporlemd  7513  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  cc2lem  7633  indv  9298  seqf1oglem2  10972  seqf1og  10973  lswwrd  11367  swrdfv  11441  swrdswrd  11493  xrnegiso  12047  summodclem3  12166  fsumf1o  12176  fsum3ser  12183  fsumadd  12192  sumsnf  12195  prodfdivap  12333  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodf1o  12374  prodsnf  12378  fprodshft  12404  fprodrev  12405  nninfctlemfo  12836  eulerthlemh  13032  eulerthlemth  13033  phisum  13042  1arithlem2  13166  ballotfilemrval  13313  ennnfonelemjn  13345  ennnfonelemp1  13349  ctiunctlemfo  13382  nninfdclemf  13392  nninfdclemp1  13393  ptex  13671  divsfval  13702  divsfvalg  13703  plusffvalg  13735  grpidvalg  13746  issubm  13832  grpinvfvalg  13900  grpinvval  13901  grpsubfvalg  13903  grplactfval  13959  mulgfvalg  13977  issubg  14029  subgex  14032  isnsg  14058  conjghm  14132  conjnmz  14135  qusghm  14138  cntzex  14144  cntrval  14145  cntzfval  14146  gzsumconst  14227  gzsummhm2  14230  gzsumshift  14233  gsumsncmn  14240  gsumzfi  14242  gsummhm2fi  14249  prdsplusgfval  14268  prdsmulrfval  14270  prdsinvlem  14280  mgpvalg  14304  srglmhm  14381  srgrmhm  14382  ringlghm  14450  ringrghm  14451  opprvalg  14458  dvdsrvald  14484  isunitd  14497  invrfvald  14513  dvrfvald  14524  issubrng  14591  issubrg  14613  rrgval  14654  rrgsupp  14658  aprval  14675  aprap  14682  aprprop  14685  scaffvalg  14727  lsssetm  14777  lspfval  14809  lspval  14811  sraval  14858  rlmvalg  14875  2idlvalg  14924  expghmap  15026  mulgghm2  15027  mulgrhm  15028  zrhvalg  15037  zrhmulg  15039  zlmval  15046  znval  15055  znzrhval  15066  aspval  15099  asclfval  15105  asclvald  15106  ntrval  15302  clsval  15303  cnpval  15390  upxp  15464  uptx  15466  txlm  15471  cnmpt11  15475  cnmpt21  15483  ispsmet  15515  mopnval  15634  bdxmet  15693  cncfmptc  15788  cncfmptid  15789  addccncf  15792  negcncf  15797  ivthdec  15836  ivthreinc  15837  hovera  15839  hoverb  15840  hoverlt1  15841  hovergt0  15842  limcmpted  15855  cnmptlimc  15866  dvrecap  15905  dveflem  15918  dvef  15919  plyval  15924  plycoeid3  15949  plyrecj  15955  log2tlbndlog2  16181  chtqcl  16205  chtqval  16206  ppiqval  16209  prmorcht  16243  sgmppw  16247  bposlem5  16276  bposlem7  16278  bposlem9  16280  lgsval  16289  lgsfvalg  16290  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  gausslemma2dlem1f1o  16345  gausslemma2dlem4  16349  lgseisenlem2  16356  2lgslem1b  16374  vtxvalg  16423  iedgvalg  16424  edgvalg  16466  edgopval  16469  edgstruct  16471  vtxdgfifival  16698  wksfval  16729  trlsfvalg  16790  clwwlkg  16800  clwwlknonmpo  16835  eupthsg  16852  depindlem1  16913  pw1map  17191  subctctexmid  17196  nninffeq  17229  nnnninfex  17231  repiecele0  17241  repiecege0  17242  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  iswomni0  17268  dceqnconst  17277  dcapnconst  17278  nconstwlpolemgt0  17281