Theorem fvmptd3 5736

Description: Deduction version of fvmpt 5719. (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 5735	. 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 4148   ` cfv 5324

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-csb 3126  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332

This theorem is referenced by:  ofvalg  6240  pw2f1odclem  7015  fival  7160  inl11  7255  djuss  7260  ctmlemr  7298  ctssdclemn0  7300  ctssdc  7303  enumctlemm  7304  nninfisollemne  7321  nninfisol  7323  fodjum  7336  fodju0  7337  ismkvnex  7345  nninfwlporlemd  7362  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  cc2lem  7475  seqf1oglem2  10772  seqf1og  10773  lswwrd  11150  swrdfv  11224  swrdswrd  11276  xrnegiso  11813  summodclem3  11931  fsumf1o  11941  fsum3ser  11948  fsumadd  11957  sumsnf  11960  prodfdivap  12098  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodf1o  12139  prodsnf  12143  fprodshft  12169  fprodrev  12170  nninfctlemfo  12601  eulerthlemh  12793  eulerthlemth  12794  phisum  12803  1arithlem2  12927  ennnfonelemjn  13013  ennnfonelemp1  13017  ctiunctlemfo  13050  nninfdclemf  13060  nninfdclemp1  13061  ptex  13337  prdsplusgfval  13357  prdsmulrfval  13359  divsfval  13401  divsfvalg  13402  plusffvalg  13435  grpidvalg  13446  issubm  13545  gsumfzz  13568  grpinvfvalg  13615  grpinvval  13616  grpsubfvalg  13618  grplactfval  13674  prdsinvlem  13681  mulgfvalg  13698  issubg  13750  subgex  13753  isnsg  13779  conjghm  13853  conjnmz  13856  qusghm  13859  gsumfzconst  13918  gsumfzmhm2  13921  mgpvalg  13926  srglmhm  13996  srgrmhm  13997  ringlghm  14064  ringrghm  14065  opprvalg  14072  dvdsrvald  14097  isunitd  14110  invrfvald  14126  dvrfvald  14137  issubrng  14203  issubrg  14225  rrgval  14266  aprval  14286  aprap  14290  scaffvalg  14310  lsssetm  14360  lspfval  14392  lspval  14394  sraval  14441  rlmvalg  14458  2idlvalg  14507  expghmap  14611  mulgghm2  14612  mulgrhm  14613  zrhvalg  14622  zrhmulg  14624  zlmval  14631  znval  14640  znzrhval  14651  ntrval  14824  clsval  14825  cnpval  14912  upxp  14986  uptx  14988  txlm  14993  cnmpt11  14997  cnmpt21  15005  ispsmet  15037  mopnval  15156  bdxmet  15215  cncfmptc  15310  cncfmptid  15311  addccncf  15314  negcncf  15319  ivthdec  15358  ivthreinc  15359  hovera  15361  hoverb  15362  hoverlt1  15363  hovergt0  15364  limcmpted  15377  cnmptlimc  15388  dvrecap  15427  dveflem  15440  dvef  15441  plyval  15446  plycoeid3  15471  plyrecj  15477  sgmppw  15706  lgsval  15723  lgsfvalg  15724  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem1f1o  15779  gausslemma2dlem4  15783  lgseisenlem2  15790  2lgslem1b  15808  vtxvalg  15857  iedgvalg  15858  edgvalg  15900  edgopval  15903  edgstruct  15905  vtxdgfifival  16097  wksfval  16119  trlsfvalg  16178  clwwlkg  16188  clwwlknonmpo  16223  eupthsg  16240  2omap  16530  pw1map  16532  subctctexmid  16537  nninffeq  16558  nnnninfex  16560  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  iswomni0  16591  dceqnconst  16600  dcapnconst  16601  nconstwlpolemgt0  16604