Theorem fvmptd3 5771

Description: Deduction version of fvmpt 5754. (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 2384	. . 3 |- F/_ x A
4		nfcv 2384	. . 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 5770	. 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 2203   |-> cmpt 4171   ` cfv 5352

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 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-csb 3139  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360

This theorem is referenced by:  ofvalg  6276  pw2f1odclem  7087  fival  7257  2omap  7269  inl11  7356  djuss  7361  ctmlemr  7399  ctssdclemn0  7401  ctssdc  7404  enumctlemm  7405  nninfisollemne  7422  nninfisol  7424  fodjum  7437  fodju0  7438  ismkvnex  7446  nninfwlporlemd  7463  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  cc2lem  7580  seqf1oglem2  10882  seqf1og  10883  lswwrd  11271  swrdfv  11345  swrdswrd  11397  xrnegiso  11947  summodclem3  12066  fsumf1o  12076  fsum3ser  12083  fsumadd  12092  sumsnf  12095  prodfdivap  12233  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodf1o  12274  prodsnf  12278  fprodshft  12304  fprodrev  12305  nninfctlemfo  12736  eulerthlemh  12928  eulerthlemth  12929  phisum  12938  1arithlem2  13062  ennnfonelemjn  13153  ennnfonelemp1  13157  ctiunctlemfo  13190  nninfdclemf  13200  nninfdclemp1  13201  ptex  13477  prdsplusgfval  13497  prdsmulrfval  13499  divsfval  13541  divsfvalg  13542  plusffvalg  13575  grpidvalg  13586  issubm  13685  gsumfzz  13708  grpinvfvalg  13755  grpinvval  13756  grpsubfvalg  13758  grplactfval  13814  prdsinvlem  13821  mulgfvalg  13838  issubg  13890  subgex  13893  isnsg  13919  conjghm  13993  conjnmz  13996  qusghm  13999  gsumfzconst  14058  gsumfzmhm2  14061  mgpvalg  14067  srglmhm  14137  srgrmhm  14138  ringlghm  14205  ringrghm  14206  opprvalg  14213  dvdsrvald  14238  isunitd  14251  invrfvald  14267  dvrfvald  14278  issubrng  14344  issubrg  14366  rrgval  14407  rrgsupp  14411  aprval  14428  aprap  14432  scaffvalg  14454  lsssetm  14504  lspfval  14536  lspval  14538  sraval  14585  rlmvalg  14602  2idlvalg  14651  expghmap  14755  mulgghm2  14756  mulgrhm  14757  zrhvalg  14766  zrhmulg  14768  zlmval  14775  znval  14784  znzrhval  14795  ntrval  14975  clsval  14976  cnpval  15063  upxp  15137  uptx  15139  txlm  15144  cnmpt11  15148  cnmpt21  15156  ispsmet  15188  mopnval  15307  bdxmet  15366  cncfmptc  15461  cncfmptid  15462  addccncf  15465  negcncf  15470  ivthdec  15509  ivthreinc  15510  hovera  15512  hoverb  15513  hoverlt1  15514  hovergt0  15515  limcmpted  15528  cnmptlimc  15539  dvrecap  15578  dveflem  15591  dvef  15592  plyval  15597  plycoeid3  15622  plyrecj  15628  sgmppw  15860  lgsval  15877  lgsfvalg  15878  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  gausslemma2dlem1f1o  15933  gausslemma2dlem4  15937  lgseisenlem2  15944  2lgslem1b  15962  vtxvalg  16011  iedgvalg  16012  edgvalg  16054  edgopval  16057  edgstruct  16059  vtxdgfifival  16286  wksfval  16317  trlsfvalg  16378  clwwlkg  16388  clwwlknonmpo  16423  eupthsg  16440  depindlem1  16501  pw1map  16769  subctctexmid  16774  nninffeq  16798  nnnninfex  16800  repiecele0  16810  repiecege0  16811  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  iswomni0  16836  dceqnconst  16846  dcapnconst  16847  nconstwlpolemgt0  16850  gsumgfsumlem  16865  gfsumsn  16867  gfsumz  16869