Theorem fvmptd3 5622

Description: Deduction version of fvmpt 5606. (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 2329	. . 3 |- F/_ x A
4		nfcv 2329	. . 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 5621	. 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 1363   e. wcel 2158   |-> cmpt 4076   ` cfv 5228

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-sbc 2975  df-csb 3070  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-iota 5190  df-fun 5230  df-fv 5236

This theorem is referenced by:  ofvalg  6106  fival  6983  inl11  7078  djuss  7083  ctmlemr  7121  ctssdclemn0  7123  ctssdc  7126  enumctlemm  7127  nninfisollemne  7143  nninfisol  7145  fodjum  7158  fodju0  7159  ismkvnex  7167  nninfwlporlemd  7184  nninfwlpoimlemg  7187  nninfwlpoimlemginf  7188  cc2lem  7279  xrnegiso  11284  summodclem3  11402  fsumf1o  11412  fsum3ser  11419  fsumadd  11428  sumsnf  11431  prodfdivap  11569  prodmodclem3  11597  prodmodclem2a  11598  fprodseq  11605  fprodf1o  11610  prodsnf  11614  fprodshft  11640  fprodrev  11641  eulerthlemh  12245  eulerthlemth  12246  phisum  12254  1arithlem2  12376  ennnfonelemjn  12417  ennnfonelemp1  12421  ctiunctlemfo  12454  nninfdclemf  12464  nninfdclemp1  12465  ptex  12731  divsfvalg  12767  plusffvalg  12800  grpidvalg  12811  issubm  12885  grpinvfvalg  12939  grpinvval  12940  grpsubfvalg  12942  grplactfval  12998  mulgfvalg  13016  issubg  13065  subgex  13068  isnsg  13094  mgpvalg  13175  srglmhm  13245  srgrmhm  13246  opprvalg  13317  reldvdsrsrg  13340  dvdsrvald  13341  isunitd  13354  invrfvald  13370  dvrfvald  13381  issubrng  13419  issubrg  13441  aprval  13471  aprap  13475  scaffvalg  13495  lsssetm  13545  lspfval  13577  lspval  13579  sraval  13626  rlmvalg  13643  2idlvalg  13690  zlmval  13785  ntrval  13906  clsval  13907  cnpval  13994  upxp  14068  uptx  14070  txlm  14075  cnmpt11  14079  cnmpt21  14087  ispsmet  14119  mopnval  14238  bdxmet  14297  cncfmptc  14378  cncfmptid  14379  addccncf  14382  negcncf  14384  ivthdec  14418  limcmpted  14428  cnmptlimc  14439  dvrecap  14473  dveflem  14483  dvef  14484  lgsval  14701  lgsfvalg  14702  lgsdir  14732  lgsdilem2  14733  lgsdi  14734  lgsne0  14735  lgseisenlem2  14747  subctctexmid  15047  nninffeq  15066  trilpolemclim  15081  trilpolemcl  15082  trilpolemisumle  15083  trilpolemeq1  15085  trilpolemlt1  15086  iswomni0  15096  dceqnconst  15105  dcapnconst  15106  nconstwlpolemgt0  15109