Theorem fvmptd3 5749

Description: Deduction version of fvmpt 5732. (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 2375	. . 3 |- F/_ x A
4		nfcv 2375	. . 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 5748	. 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 2202   |-> cmpt 4155   ` cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-csb 3129  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341

This theorem is referenced by:  ofvalg  6254  pw2f1odclem  7063  fival  7212  inl11  7307  djuss  7312  ctmlemr  7350  ctssdclemn0  7352  ctssdc  7355  enumctlemm  7356  nninfisollemne  7373  nninfisol  7375  fodjum  7388  fodju0  7389  ismkvnex  7397  nninfwlporlemd  7414  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  cc2lem  7528  seqf1oglem2  10828  seqf1og  10829  lswwrd  11209  swrdfv  11283  swrdswrd  11335  xrnegiso  11885  summodclem3  12004  fsumf1o  12014  fsum3ser  12021  fsumadd  12030  sumsnf  12033  prodfdivap  12171  prodmodclem3  12199  prodmodclem2a  12200  fprodseq  12207  fprodf1o  12212  prodsnf  12216  fprodshft  12242  fprodrev  12243  nninfctlemfo  12674  eulerthlemh  12866  eulerthlemth  12867  phisum  12876  1arithlem2  13000  ennnfonelemjn  13086  ennnfonelemp1  13090  ctiunctlemfo  13123  nninfdclemf  13133  nninfdclemp1  13134  ptex  13410  prdsplusgfval  13430  prdsmulrfval  13432  divsfval  13474  divsfvalg  13475  plusffvalg  13508  grpidvalg  13519  issubm  13618  gsumfzz  13641  grpinvfvalg  13688  grpinvval  13689  grpsubfvalg  13691  grplactfval  13747  prdsinvlem  13754  mulgfvalg  13771  issubg  13823  subgex  13826  isnsg  13852  conjghm  13926  conjnmz  13929  qusghm  13932  gsumfzconst  13991  gsumfzmhm2  13994  mgpvalg  14000  srglmhm  14070  srgrmhm  14071  ringlghm  14138  ringrghm  14139  opprvalg  14146  dvdsrvald  14171  isunitd  14184  invrfvald  14200  dvrfvald  14211  issubrng  14277  issubrg  14299  rrgval  14340  rrgsupp  14344  aprval  14361  aprap  14365  scaffvalg  14385  lsssetm  14435  lspfval  14467  lspval  14469  sraval  14516  rlmvalg  14533  2idlvalg  14582  expghmap  14686  mulgghm2  14687  mulgrhm  14688  zrhvalg  14697  zrhmulg  14699  zlmval  14706  znval  14715  znzrhval  14726  ntrval  14904  clsval  14905  cnpval  14992  upxp  15066  uptx  15068  txlm  15073  cnmpt11  15077  cnmpt21  15085  ispsmet  15117  mopnval  15236  bdxmet  15295  cncfmptc  15390  cncfmptid  15391  addccncf  15394  negcncf  15399  ivthdec  15438  ivthreinc  15439  hovera  15441  hoverb  15442  hoverlt1  15443  hovergt0  15444  limcmpted  15457  cnmptlimc  15468  dvrecap  15507  dveflem  15520  dvef  15521  plyval  15526  plycoeid3  15551  plyrecj  15557  sgmppw  15789  lgsval  15806  lgsfvalg  15807  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  gausslemma2dlem1f1o  15862  gausslemma2dlem4  15866  lgseisenlem2  15873  2lgslem1b  15891  vtxvalg  15940  iedgvalg  15941  edgvalg  15983  edgopval  15986  edgstruct  15988  vtxdgfifival  16215  wksfval  16246  trlsfvalg  16307  clwwlkg  16317  clwwlknonmpo  16352  eupthsg  16369  depindlem1  16430  2omap  16698  pw1map  16700  subctctexmid  16705  nninffeq  16729  nnnninfex  16731  repiecele0  16741  repiecege0  16742  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  iswomni0  16767  dceqnconst  16776  dcapnconst  16777  nconstwlpolemgt0  16780  gsumgfsumlem  16795  gfsumsn  16797