Theorem fvmptd3 5611

Description: Deduction version of fvmpt 5595. (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 2319	. . 3 |- F/_ x A
4		nfcv 2319	. . 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 5610	. 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 1353   e. wcel 2148   |-> cmpt 4066   ` cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226

This theorem is referenced by:  ofvalg  6094  fival  6971  inl11  7066  djuss  7071  ctmlemr  7109  ctssdclemn0  7111  ctssdc  7114  enumctlemm  7115  nninfisollemne  7131  nninfisol  7133  fodjum  7146  fodju0  7147  ismkvnex  7155  nninfwlporlemd  7172  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  cc2lem  7267  xrnegiso  11272  summodclem3  11390  fsumf1o  11400  fsum3ser  11407  fsumadd  11416  sumsnf  11419  prodfdivap  11557  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  fprodf1o  11598  prodsnf  11602  fprodshft  11628  fprodrev  11629  eulerthlemh  12233  eulerthlemth  12234  phisum  12242  1arithlem2  12364  ennnfonelemjn  12405  ennnfonelemp1  12409  ctiunctlemfo  12442  nninfdclemf  12452  nninfdclemp1  12453  ptex  12718  divsfvalg  12753  plusffvalg  12786  grpidvalg  12797  issubm  12868  grpinvfvalg  12920  grpinvval  12921  grpsubfvalg  12923  grplactfval  12976  mulgfvalg  12990  issubg  13038  subgex  13041  isnsg  13067  mgpvalg  13138  srglmhm  13181  srgrmhm  13182  opprvalg  13246  reldvdsrsrg  13266  dvdsrvald  13267  isunitd  13280  invrfvald  13296  dvrfvald  13307  issubrg  13347  aprval  13377  aprap  13381  scaffvalg  13401  lsssetm  13449  lspfval  13480  lspval  13482  ntrval  13695  clsval  13696  cnpval  13783  upxp  13857  uptx  13859  txlm  13864  cnmpt11  13868  cnmpt21  13876  ispsmet  13908  mopnval  14027  bdxmet  14086  cncfmptc  14167  cncfmptid  14168  addccncf  14171  negcncf  14173  ivthdec  14207  limcmpted  14217  cnmptlimc  14228  dvrecap  14262  dveflem  14272  dvef  14273  lgsval  14490  lgsfvalg  14491  lgsdir  14521  lgsdilem2  14522  lgsdi  14523  lgsne0  14524  lgseisenlem2  14536  subctctexmid  14835  nninffeq  14854  trilpolemclim  14869  trilpolemcl  14870  trilpolemisumle  14871  trilpolemeq1  14873  trilpolemlt1  14874  iswomni0  14884  dceqnconst  14893  dcapnconst  14894  nconstwlpolemgt0  14897