Theorem fvmptd3 5610

Description: Deduction version of fvmpt 5594. (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 5609	. 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 4065   ` cfv 5217

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 4122  ax-pow 4175  ax-pr 4210

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 2740  df-sbc 2964  df-csb 3059  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-iota 5179  df-fun 5219  df-fv 5225

This theorem is referenced by:  ofvalg  6092  fival  6969  inl11  7064  djuss  7069  ctmlemr  7107  ctssdclemn0  7109  ctssdc  7112  enumctlemm  7113  nninfisollemne  7129  nninfisol  7131  fodjum  7144  fodju0  7145  ismkvnex  7153  nninfwlporlemd  7170  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  cc2lem  7265  xrnegiso  11270  summodclem3  11388  fsumf1o  11398  fsum3ser  11405  fsumadd  11414  sumsnf  11417  prodfdivap  11555  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  fprodf1o  11596  prodsnf  11600  fprodshft  11626  fprodrev  11627  eulerthlemh  12231  eulerthlemth  12232  phisum  12240  1arithlem2  12362  ennnfonelemjn  12403  ennnfonelemp1  12407  ctiunctlemfo  12440  nninfdclemf  12450  nninfdclemp1  12451  ptex  12713  divsfvalg  12748  plusffvalg  12781  grpidvalg  12792  issubm  12863  grpinvfvalg  12915  grpinvval  12916  grpsubfvalg  12918  grplactfval  12971  mulgfvalg  12985  issubg  13033  subgex  13036  isnsg  13062  mgpvalg  13133  srglmhm  13176  srgrmhm  13177  opprvalg  13241  reldvdsrsrg  13261  dvdsrvald  13262  isunitd  13275  invrfvald  13291  dvrfvald  13302  issubrg  13342  aprval  13372  aprap  13376  scaffvalg  13396  ntrval  13613  clsval  13614  cnpval  13701  upxp  13775  uptx  13777  txlm  13782  cnmpt11  13786  cnmpt21  13794  ispsmet  13826  mopnval  13945  bdxmet  14004  cncfmptc  14085  cncfmptid  14086  addccncf  14089  negcncf  14091  ivthdec  14125  limcmpted  14135  cnmptlimc  14146  dvrecap  14180  dveflem  14190  dvef  14191  lgsval  14408  lgsfvalg  14409  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgseisenlem2  14454  subctctexmid  14753  nninffeq  14772  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  iswomni0  14802  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814