Theorem fvmptd3 5799

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

Hypotheses

Ref	Expression
fvmptd3.1	|- F = ( x e. D |-> B )
fvmptd3.2	|- ( x = A -> B = C )
fvmptd3.3	|- ( ph -> A e. D )
fvmptd3.4	|- ( ph -> C e. V )

Assertion

Ref	Expression
fvmptd3	|- ( ph -> ( F ` A ) = C )

Distinct variable groups:   x, A   x, C   x, D

Allowed substitution hints:   ph( x)   B( x)   F( x)   V( x)

Proof of Theorem fvmptd3

Step	Hyp	Ref	Expression
1		fvmptd3.3	. 2 |- ( ph -> A e. D )
2		fvmptd3.4	. 2 |- ( ph -> C e. V )
3		nfcv 2392	. . 3 |- F/_ x A
4		nfcv 2392	. . 3 |- F/_ x C
5		fvmptd3.2	. . 3 |- ( x = A -> B = C )
6		fvmptd3.1	. . 3 |- F = ( x e. D |-> B )
7	3, 4, 5, 6	fvmptf 5798	. 2 |- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )
8	1, 2, 7	syl2anc 415	1 |- ( ph -> ( F ` A ) = C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. 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  7318  inl11  7405  djuss  7410  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  nninfisollemne  7471  nninfisol  7473  fodjum  7486  fodju0  7487  ismkvnex  7495  nninfwlporlemd  7512  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  cc2lem  7632  indv  9297  seqf1oglem2  10970  seqf1og  10971  lswwrd  11365  swrdfv  11439  swrdswrd  11491  xrnegiso  12044  summodclem3  12163  fsumf1o  12173  fsum3ser  12180  fsumadd  12189  sumsnf  12192  prodfdivap  12330  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodf1o  12371  prodsnf  12375  fprodshft  12401  fprodrev  12402  nninfctlemfo  12833  eulerthlemh  13029  eulerthlemth  13030  phisum  13039  1arithlem2  13163  ballotfilemrval  13310  ennnfonelemjn  13342  ennnfonelemp1  13346  ctiunctlemfo  13379  nninfdclemf  13389  nninfdclemp1  13390  ptex  13667  divsfval  13698  divsfvalg  13699  plusffvalg  13731  grpidvalg  13742  issubm  13828  grpinvfvalg  13896  grpinvval  13897  grpsubfvalg  13899  grplactfval  13955  mulgfvalg  13973  issubg  14025  subgex  14028  isnsg  14054  conjghm  14128  conjnmz  14131  qusghm  14134  gzsumconst  14192  gzsummhm2  14195  gzsumshift  14198  gsumsncmn  14205  gsumzfi  14207  gsummhm2fi  14214  prdsplusgfval  14233  prdsmulrfval  14235  prdsinvlem  14245  mgpvalg  14269  srglmhm  14346  srgrmhm  14347  ringlghm  14415  ringrghm  14416  opprvalg  14423  dvdsrvald  14449  isunitd  14462  invrfvald  14478  dvrfvald  14489  issubrng  14556  issubrg  14578  rrgval  14619  rrgsupp  14623  aprval  14640  aprap  14647  aprprop  14650  scaffvalg  14692  lsssetm  14742  lspfval  14774  lspval  14776  sraval  14823  rlmvalg  14840  2idlvalg  14889  expghmap  14991  mulgghm2  14992  mulgrhm  14993  zrhvalg  15002  zrhmulg  15004  zlmval  15011  znval  15020  znzrhval  15031  aspval  15064  asclfval  15070  asclvald  15071  ntrval  15260  clsval  15261  cnpval  15348  upxp  15422  uptx  15424  txlm  15429  cnmpt11  15433  cnmpt21  15441  ispsmet  15473  mopnval  15592  bdxmet  15651  cncfmptc  15746  cncfmptid  15747  addccncf  15750  negcncf  15755  ivthdec  15794  ivthreinc  15795  hovera  15797  hoverb  15798  hoverlt1  15799  hovergt0  15800  limcmpted  15813  cnmptlimc  15824  dvrecap  15863  dveflem  15876  dvef  15877  plyval  15882  plycoeid3  15907  plyrecj  15913  log2tlbndlog2  16139  ppiqval  16160  sgmppw  16187  bposlem5  16213  lgsval  16221  lgsfvalg  16222  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  gausslemma2dlem1f1o  16277  gausslemma2dlem4  16281  lgseisenlem2  16288  2lgslem1b  16306  vtxvalg  16355  iedgvalg  16356  edgvalg  16398  edgopval  16401  edgstruct  16403  vtxdgfifival  16630  wksfval  16661  trlsfvalg  16722  clwwlkg  16732  clwwlknonmpo  16767  eupthsg  16784  depindlem1  16845  pw1map  17123  subctctexmid  17128  nninffeq  17161  nnnninfex  17163  repiecele0  17173  repiecege0  17174  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  iswomni0  17199  dceqnconst  17208  dcapnconst  17209  nconstwlpolemgt0  17212