Theorem fvmptd3 5802

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209   |-> cmpt 4193   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388

This theorem is used by:  ofvalg  6316  pw2f1odclem  7140  fival  7309  2omap  7324  inl11  7411  djuss  7416  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  nninfisollemne  7477  nninfisol  7479  fodjum  7492  fodju0  7493  ismkvnex  7501  nninfwlporlemd  7518  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  cc2lem  7638  indv  9304  seqf1oglem2  10977  seqf1og  10978  lswwrd  11372  swrdfv  11446  swrdswrd  11498  xrnegiso  12052  summodclem3  12171  fsumf1o  12181  fsum3ser  12188  fsumadd  12197  sumsnf  12200  prodfdivap  12338  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodf1o  12379  prodsnf  12383  fprodshft  12409  fprodrev  12410  nninfctlemfo  12841  eulerthlemh  13037  eulerthlemth  13038  phisum  13047  1arithlem2  13171  ballotfilemrval  13318  ennnfonelemjn  13350  ennnfonelemp1  13354  ctiunctlemfo  13387  nninfdclemf  13397  nninfdclemp1  13398  ptex  13676  divsfval  13707  divsfvalg  13708  plusffvalg  13740  grpidvalg  13751  issubm  13837  grpinvfvalg  13905  grpinvval  13906  grpsubfvalg  13908  grplactfval  13964  mulgfvalg  13982  issubg  14034  subgex  14037  isnsg  14063  conjghm  14137  conjnmz  14140  qusghm  14143  cntzex  14149  cntrval  14150  cntzfval  14151  gzsumconst  14232  gzsummhm2  14235  gzsumshift  14238  gsumsncmn  14245  gsumzfi  14247  gsummhm2fi  14264  gsum2dfi  14272  prdsplusgfval  14290  prdsmulrfval  14292  prdsinvlem  14302  mgpvalg  14326  srglmhm  14403  srgrmhm  14404  ringlghm  14472  ringrghm  14473  opprvalg  14482  dvdsrvald  14508  isunitd  14521  invrfvald  14537  dvrfvald  14548  issubrng  14615  issubrg  14637  rrgval  14678  rrgsupp  14682  aprval  14699  aprap  14706  aprprop  14709  scaffvalg  14751  lsssetm  14801  lspfval  14833  lspval  14835  sraval  14882  rlmvalg  14899  2idlvalg  14948  expghmap  15050  mulgghm2  15051  mulgrhm  15052  zrhvalg  15061  zrhmulg  15063  zlmval  15070  znval  15079  znzrhval  15090  aspval  15123  asclfval  15129  asclvald  15130  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psrlidmfi  15208  psrridmfi  15209  mvrval  15215  mvrval2  15216  ntrval  15353  clsval  15354  cnpval  15441  upxp  15515  uptx  15517  txlm  15522  cnmpt11  15526  cnmpt21  15534  ispsmet  15566  mopnval  15685  bdxmet  15744  cncfmptc  15839  cncfmptid  15840  addccncf  15843  negcncf  15848  ivthdec  15887  ivthreinc  15888  hovera  15890  hoverb  15891  hoverlt1  15892  hovergt0  15893  limcmpted  15906  cnmptlimc  15917  dvrecap  15956  dveflem  15969  dvef  15970  plyval  15975  plycoeid3  16000  plyrecj  16006  log2tlbndlog2  16237  chtqcl  16261  chtqval  16262  ppiqval  16265  prmorcht  16299  sgmppw  16303  bposlem5  16332  bposlem7  16334  bposlem9  16336  lgsval  16345  lgsfvalg  16346  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  gausslemma2dlem1f1o  16401  gausslemma2dlem4  16405  lgseisenlem2  16412  2lgslem1b  16430  vtxvalg  16479  iedgvalg  16480  edgvalg  16522  edgopval  16525  edgstruct  16527  vtxdgfifival  16754  wksfval  16785  trlsfvalg  16846  clwwlkg  16856  clwwlknonmpo  16891  eupthsg  16908  depindlem1  16969  pw1map  17247  subctctexmid  17252  nninffeq  17286  nnnninfex  17288  repiecele0  17298  repiecege0  17299  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  iswomni0  17325  dceqnconst  17334  dcapnconst  17335  nconstwlpolemgt0  17338