Theorem fvmptd3 5651

Description: Deduction version of fvmpt 5634. (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 2336	. . 3 |- F/_ x A
4		nfcv 2336	. . 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 5650	. 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 1364   e. wcel 2164   |-> cmpt 4090   ` cfv 5254

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2986  df-csb 3081  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262

This theorem is referenced by:  ofvalg  6140  pw2f1odclem  6890  fival  7029  inl11  7124  djuss  7129  ctmlemr  7167  ctssdclemn0  7169  ctssdc  7172  enumctlemm  7173  nninfisollemne  7190  nninfisol  7192  fodjum  7205  fodju0  7206  ismkvnex  7214  nninfwlporlemd  7231  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  cc2lem  7326  seqf1oglem2  10591  seqf1og  10592  xrnegiso  11405  summodclem3  11523  fsumf1o  11533  fsum3ser  11540  fsumadd  11549  sumsnf  11552  prodfdivap  11690  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodf1o  11731  prodsnf  11735  fprodshft  11761  fprodrev  11762  nninfctlemfo  12177  eulerthlemh  12369  eulerthlemth  12370  phisum  12378  1arithlem2  12502  ennnfonelemjn  12559  ennnfonelemp1  12563  ctiunctlemfo  12596  nninfdclemf  12606  nninfdclemp1  12607  ptex  12875  divsfval  12911  divsfvalg  12912  plusffvalg  12945  grpidvalg  12956  issubm  13044  gsumfzz  13067  grpinvfvalg  13114  grpinvval  13115  grpsubfvalg  13117  grplactfval  13173  mulgfvalg  13191  issubg  13243  subgex  13246  isnsg  13272  conjghm  13346  conjnmz  13349  qusghm  13352  gsumfzconst  13411  gsumfzmhm2  13414  mgpvalg  13419  srglmhm  13489  srgrmhm  13490  ringlghm  13557  ringrghm  13558  opprvalg  13565  reldvdsrsrg  13588  dvdsrvald  13589  isunitd  13602  invrfvald  13618  dvrfvald  13629  issubrng  13695  issubrg  13717  rrgval  13758  aprval  13778  aprap  13782  scaffvalg  13802  lsssetm  13852  lspfval  13884  lspval  13886  sraval  13933  rlmvalg  13950  2idlvalg  13999  expghmap  14095  mulgghm2  14096  mulgrhm  14097  zrhvalg  14106  zrhmulg  14108  zlmval  14115  znval  14124  znzrhval  14135  ntrval  14278  clsval  14279  cnpval  14366  upxp  14440  uptx  14442  txlm  14447  cnmpt11  14451  cnmpt21  14459  ispsmet  14491  mopnval  14610  bdxmet  14669  cncfmptc  14750  cncfmptid  14751  addccncf  14754  negcncf  14759  ivthdec  14798  ivthreinc  14799  hovera  14801  hoverb  14802  hoverlt1  14803  hovergt0  14804  limcmpted  14817  cnmptlimc  14828  dvrecap  14862  dveflem  14872  dvef  14873  plyval  14878  lgsval  15120  lgsfvalg  15121  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  gausslemma2dlem1f1o  15176  gausslemma2dlem4  15180  lgseisenlem2  15187  subctctexmid  15491  nninffeq  15510  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  iswomni0  15541  dceqnconst  15550  dcapnconst  15551  nconstwlpolemgt0  15554