Theorem fvmptd3 5776

Description: Deduction version of fvmpt 5759. (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 2386	. . 3 |- F/_ x A
4		nfcv 2386	. . 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 5775	. 2 |- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )
8	1, 2, 7	syl2anc 411	1 |- ( ph -> ( F ` A ) = C )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205   |-> cmpt 4176   ` cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-csb 3142  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365

This theorem is referenced by:  ofvalg  6285  pw2f1odclem  7100  fival  7270  2omap  7282  inl11  7369  djuss  7374  ctmlemr  7412  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  nninfisollemne  7435  nninfisol  7437  fodjum  7450  fodju0  7451  ismkvnex  7459  nninfwlporlemd  7476  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  cc2lem  7596  seqf1oglem2  10906  seqf1og  10907  lswwrd  11296  swrdfv  11370  swrdswrd  11422  xrnegiso  11972  summodclem3  12091  fsumf1o  12101  fsum3ser  12108  fsumadd  12117  sumsnf  12120  prodfdivap  12258  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodf1o  12299  prodsnf  12303  fprodshft  12329  fprodrev  12330  nninfctlemfo  12761  eulerthlemh  12953  eulerthlemth  12954  phisum  12963  1arithlem2  13087  ballotfilemrval  13205  ennnfonelemjn  13237  ennnfonelemp1  13241  ctiunctlemfo  13274  nninfdclemf  13284  nninfdclemp1  13285  ptex  13561  divsfval  13592  divsfvalg  13593  plusffvalg  13625  grpidvalg  13636  issubm  13727  gsumfzz  13750  grpinvfvalg  13797  grpinvval  13798  grpsubfvalg  13800  grplactfval  13856  mulgfvalg  13874  issubg  13926  subgex  13929  isnsg  13955  conjghm  14029  conjnmz  14032  qusghm  14035  gsumfzconst  14094  gsumfzmhm2  14097  gsumshift  14105  gfsumsn  14107  gfsumz  14109  prdsplusgfval  14126  prdsmulrfval  14128  prdsinvlem  14138  mgpvalg  14162  srglmhm  14236  srgrmhm  14237  ringlghm  14304  ringrghm  14305  opprvalg  14312  dvdsrvald  14338  isunitd  14351  invrfvald  14367  dvrfvald  14378  issubrng  14445  issubrg  14467  rrgval  14508  rrgsupp  14512  aprval  14529  aprap  14536  aprprop  14539  scaffvalg  14580  lsssetm  14630  lspfval  14662  lspval  14664  sraval  14711  rlmvalg  14728  2idlvalg  14777  expghmap  14881  mulgghm2  14882  mulgrhm  14883  zrhvalg  14892  zrhmulg  14894  zlmval  14901  znval  14910  znzrhval  14921  ntrval  15101  clsval  15102  cnpval  15189  upxp  15263  uptx  15265  txlm  15270  cnmpt11  15274  cnmpt21  15282  ispsmet  15314  mopnval  15433  bdxmet  15492  cncfmptc  15587  cncfmptid  15588  addccncf  15591  negcncf  15596  ivthdec  15635  ivthreinc  15636  hovera  15638  hoverb  15639  hoverlt1  15640  hovergt0  15641  limcmpted  15654  cnmptlimc  15665  dvrecap  15704  dveflem  15717  dvef  15718  plyval  15723  plycoeid3  15748  plyrecj  15754  sgmppw  15986  lgsval  16003  lgsfvalg  16004  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  gausslemma2dlem1f1o  16059  gausslemma2dlem4  16063  lgseisenlem2  16070  2lgslem1b  16088  vtxvalg  16137  iedgvalg  16138  edgvalg  16180  edgopval  16183  edgstruct  16185  vtxdgfifival  16412  wksfval  16443  trlsfvalg  16504  clwwlkg  16514  clwwlknonmpo  16549  eupthsg  16566  depindlem1  16627  pw1map  16895  subctctexmid  16900  nninffeq  16924  nnnninfex  16926  repiecele0  16936  repiecege0  16937  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  iswomni0  16962  dceqnconst  16972  dcapnconst  16973  nconstwlpolemgt0  16976