Theorem fvmptd3 5799

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209   |-> cmpt 4192   ` cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385

This theorem is used by:  ofvalg  6312  pw2f1odclem  7134  fival  7304  2omap  7319  inl11  7406  djuss  7411  ctmlemr  7449  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  nninfisollemne  7472  nninfisol  7474  fodjum  7487  fodju0  7488  ismkvnex  7496  nninfwlporlemd  7513  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  cc2lem  7633  indv  9298  seqf1oglem2  10972  seqf1og  10973  lswwrd  11367  swrdfv  11441  swrdswrd  11493  xrnegiso  12047  summodclem3  12166  fsumf1o  12176  fsum3ser  12183  fsumadd  12192  sumsnf  12195  prodfdivap  12333  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodf1o  12374  prodsnf  12378  fprodshft  12404  fprodrev  12405  nninfctlemfo  12836  eulerthlemh  13032  eulerthlemth  13033  phisum  13042  1arithlem2  13166  ballotfilemrval  13313  ennnfonelemjn  13345  ennnfonelemp1  13349  ctiunctlemfo  13382  nninfdclemf  13392  nninfdclemp1  13393  ptex  13671  divsfval  13702  divsfvalg  13703  plusffvalg  13735  grpidvalg  13746  issubm  13832  grpinvfvalg  13900  grpinvval  13901  grpsubfvalg  13903  grplactfval  13959  mulgfvalg  13977  issubg  14029  subgex  14032  isnsg  14058  conjghm  14132  conjnmz  14135  qusghm  14138  cntzex  14144  cntrval  14145  cntzfval  14146  gzsumconst  14227  gzsummhm2  14230  gzsumshift  14233  gsumsncmn  14240  gsumzfi  14242  gsummhm2fi  14256  prdsplusgfval  14275  prdsmulrfval  14277  prdsinvlem  14287  mgpvalg  14311  srglmhm  14388  srgrmhm  14389  ringlghm  14457  ringrghm  14458  opprvalg  14465  dvdsrvald  14491  isunitd  14504  invrfvald  14520  dvrfvald  14531  issubrng  14598  issubrg  14620  rrgval  14661  rrgsupp  14665  aprval  14682  aprap  14689  aprprop  14692  scaffvalg  14734  lsssetm  14784  lspfval  14816  lspval  14818  sraval  14865  rlmvalg  14882  2idlvalg  14931  expghmap  15033  mulgghm2  15034  mulgrhm  15035  zrhvalg  15044  zrhmulg  15046  zlmval  15053  znval  15062  znzrhval  15073  aspval  15106  asclfval  15112  asclvald  15113  psrlidmfi  15178  ntrval  15310  clsval  15311  cnpval  15398  upxp  15472  uptx  15474  txlm  15479  cnmpt11  15483  cnmpt21  15491  ispsmet  15523  mopnval  15642  bdxmet  15701  cncfmptc  15796  cncfmptid  15797  addccncf  15800  negcncf  15805  ivthdec  15844  ivthreinc  15845  hovera  15847  hoverb  15848  hoverlt1  15849  hovergt0  15850  limcmpted  15863  cnmptlimc  15874  dvrecap  15913  dveflem  15926  dvef  15927  plyval  15932  plycoeid3  15957  plyrecj  15963  log2tlbndlog2  16194  chtqcl  16218  chtqval  16219  ppiqval  16222  prmorcht  16256  sgmppw  16260  bposlem5  16289  bposlem7  16291  bposlem9  16293  lgsval  16302  lgsfvalg  16303  lgsdir  16333  lgsdilem2  16334  lgsdi  16335  lgsne0  16336  gausslemma2dlem1f1o  16358  gausslemma2dlem4  16362  lgseisenlem2  16369  2lgslem1b  16387  vtxvalg  16436  iedgvalg  16437  edgvalg  16479  edgopval  16482  edgstruct  16484  vtxdgfifival  16711  wksfval  16742  trlsfvalg  16803  clwwlkg  16813  clwwlknonmpo  16848  eupthsg  16865  depindlem1  16926  pw1map  17204  subctctexmid  17209  nninffeq  17242  nnnninfex  17244  repiecele0  17254  repiecege0  17255  trilpolemclim  17265  trilpolemcl  17266  trilpolemisumle  17267  trilpolemeq1  17269  trilpolemlt1  17270  iswomni0  17281  dceqnconst  17290  dcapnconst  17291  nconstwlpolemgt0  17294