Theorem fvmptd3 5579

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136   |-> cmpt 4043   ` cfv 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-v 2728  df-sbc 2952  df-csb 3046  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-opab 4044  df-mpt 4045  df-id 4271  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-iota 5153  df-fun 5190  df-fv 5196

This theorem is referenced by:  ofvalg  6059  fival  6935  inl11  7030  djuss  7035  ctmlemr  7073  ctssdclemn0  7075  ctssdc  7078  enumctlemm  7079  nninfisollemne  7095  nninfisol  7097  fodjum  7110  fodju0  7111  ismkvnex  7119  cc2lem  7207  xrnegiso  11203  summodclem3  11321  fsumf1o  11331  fsum3ser  11338  fsumadd  11347  sumsnf  11350  prodfdivap  11488  prodmodclem3  11516  prodmodclem2a  11517  fprodseq  11524  fprodf1o  11529  prodsnf  11533  fprodshft  11559  fprodrev  11560  eulerthlemh  12163  eulerthlemth  12164  phisum  12172  1arithlem2  12294  ennnfonelemjn  12335  ennnfonelemp1  12339  ctiunctlemfo  12372  nninfdclemf  12382  nninfdclemp1  12383  plusffvalg  12593  grpidvalg  12604  ntrval  12750  clsval  12751  cnpval  12838  upxp  12912  uptx  12914  txlm  12919  cnmpt11  12923  cnmpt21  12931  ispsmet  12963  mopnval  13082  bdxmet  13141  cncfmptc  13222  cncfmptid  13223  addccncf  13226  negcncf  13228  ivthdec  13262  limcmpted  13272  cnmptlimc  13283  dvrecap  13317  dveflem  13327  dvef  13328  lgsval  13545  lgsfvalg  13546  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  subctctexmid  13881  nninffeq  13900  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  iswomni0  13930  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942