Theorem fvmptd3 5728

Description: Deduction version of fvmpt 5711. (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 2372	. . 3 |- F/_ x A
4		nfcv 2372	. . 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 5727	. 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 1395   e. wcel 2200   |-> cmpt 4145   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-csb 3125  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326

This theorem is referenced by:  ofvalg  6228  pw2f1odclem  6995  fival  7137  inl11  7232  djuss  7237  ctmlemr  7275  ctssdclemn0  7277  ctssdc  7280  enumctlemm  7281  nninfisollemne  7298  nninfisol  7300  fodjum  7313  fodju0  7314  ismkvnex  7322  nninfwlporlemd  7339  nninfwlpoimlemg  7342  nninfwlpoimlemginf  7343  cc2lem  7452  seqf1oglem2  10742  seqf1og  10743  lswwrd  11118  swrdfv  11185  swrdswrd  11237  xrnegiso  11773  summodclem3  11891  fsumf1o  11901  fsum3ser  11908  fsumadd  11917  sumsnf  11920  prodfdivap  12058  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodf1o  12099  prodsnf  12103  fprodshft  12129  fprodrev  12130  nninfctlemfo  12561  eulerthlemh  12753  eulerthlemth  12754  phisum  12763  1arithlem2  12887  ennnfonelemjn  12973  ennnfonelemp1  12977  ctiunctlemfo  13010  nninfdclemf  13020  nninfdclemp1  13021  ptex  13297  prdsplusgfval  13317  prdsmulrfval  13319  divsfval  13361  divsfvalg  13362  plusffvalg  13395  grpidvalg  13406  issubm  13505  gsumfzz  13528  grpinvfvalg  13575  grpinvval  13576  grpsubfvalg  13578  grplactfval  13634  prdsinvlem  13641  mulgfvalg  13658  issubg  13710  subgex  13713  isnsg  13739  conjghm  13813  conjnmz  13816  qusghm  13819  gsumfzconst  13878  gsumfzmhm2  13881  mgpvalg  13886  srglmhm  13956  srgrmhm  13957  ringlghm  14024  ringrghm  14025  opprvalg  14032  dvdsrvald  14057  isunitd  14070  invrfvald  14086  dvrfvald  14097  issubrng  14163  issubrg  14185  rrgval  14226  aprval  14246  aprap  14250  scaffvalg  14270  lsssetm  14320  lspfval  14352  lspval  14354  sraval  14401  rlmvalg  14418  2idlvalg  14467  expghmap  14571  mulgghm2  14572  mulgrhm  14573  zrhvalg  14582  zrhmulg  14584  zlmval  14591  znval  14600  znzrhval  14611  ntrval  14784  clsval  14785  cnpval  14872  upxp  14946  uptx  14948  txlm  14953  cnmpt11  14957  cnmpt21  14965  ispsmet  14997  mopnval  15116  bdxmet  15175  cncfmptc  15270  cncfmptid  15271  addccncf  15274  negcncf  15279  ivthdec  15318  ivthreinc  15319  hovera  15321  hoverb  15322  hoverlt1  15323  hovergt0  15324  limcmpted  15337  cnmptlimc  15348  dvrecap  15387  dveflem  15400  dvef  15401  plyval  15406  plycoeid3  15431  plyrecj  15437  sgmppw  15666  lgsval  15683  lgsfvalg  15684  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  gausslemma2dlem1f1o  15739  gausslemma2dlem4  15743  lgseisenlem2  15750  2lgslem1b  15768  vtxvalg  15817  iedgvalg  15818  edgvalg  15860  edgopval  15862  edgstruct  15864  wksfval  16035  2omap  16359  pw1map  16361  subctctexmid  16366  nninffeq  16386  nnnninfex  16388  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  iswomni0  16419  dceqnconst  16428  dcapnconst  16429  nconstwlpolemgt0  16432