Theorem fvmptd3 5799

Description: Deduction version of fvmpt 5782. (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 5798	. 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 4192   ` cfv 5377

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 4249  ax-pow 4311  ax-pr 4346

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 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385

This theorem is used by:  ofvalg  6312  pw2f1odclem  7134  fival  7304  2omap  7318  inl11  7405  djuss  7410  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  nninfisollemne  7471  nninfisol  7473  fodjum  7486  fodju0  7487  ismkvnex  7495  nninfwlporlemd  7512  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  cc2lem  7632  indv  9295  seqf1oglem2  10957  seqf1og  10958  lswwrd  11351  swrdfv  11425  swrdswrd  11477  xrnegiso  12028  summodclem3  12147  fsumf1o  12157  fsum3ser  12164  fsumadd  12173  sumsnf  12176  prodfdivap  12314  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  fprodf1o  12355  prodsnf  12359  fprodshft  12385  fprodrev  12386  nninfctlemfo  12817  eulerthlemh  13009  eulerthlemth  13010  phisum  13019  1arithlem2  13143  ballotfilemrval  13261  ennnfonelemjn  13293  ennnfonelemp1  13297  ctiunctlemfo  13330  nninfdclemf  13340  nninfdclemp1  13341  ptex  13618  divsfval  13649  divsfvalg  13650  plusffvalg  13682  grpidvalg  13693  issubm  13779  grpinvfvalg  13847  grpinvval  13848  grpsubfvalg  13850  grplactfval  13906  mulgfvalg  13924  issubg  13976  subgex  13979  isnsg  14005  conjghm  14079  conjnmz  14082  qusghm  14085  gzsumconst  14143  gzsummhm2  14146  gzsumshift  14149  gsumsncmn  14156  gsumzfi  14158  gsummhm2fi  14165  prdsplusgfval  14184  prdsmulrfval  14186  prdsinvlem  14196  mgpvalg  14220  srglmhm  14297  srgrmhm  14298  ringlghm  14366  ringrghm  14367  opprvalg  14374  dvdsrvald  14400  isunitd  14413  invrfvald  14429  dvrfvald  14440  issubrng  14507  issubrg  14529  rrgval  14570  rrgsupp  14574  aprval  14591  aprap  14598  aprprop  14601  scaffvalg  14643  lsssetm  14693  lspfval  14725  lspval  14727  sraval  14774  rlmvalg  14791  2idlvalg  14840  expghmap  14942  mulgghm2  14943  mulgrhm  14944  zrhvalg  14953  zrhmulg  14955  zlmval  14962  znval  14971  znzrhval  14982  aspval  15015  asclfval  15021  asclvald  15022  ntrval  15211  clsval  15212  cnpval  15299  upxp  15373  uptx  15375  txlm  15380  cnmpt11  15384  cnmpt21  15392  ispsmet  15424  mopnval  15543  bdxmet  15602  cncfmptc  15697  cncfmptid  15698  addccncf  15701  negcncf  15706  ivthdec  15745  ivthreinc  15746  hovera  15748  hoverb  15749  hoverlt1  15750  hovergt0  15751  limcmpted  15764  cnmptlimc  15775  dvrecap  15814  dveflem  15827  dvef  15828  plyval  15833  plycoeid3  15858  plyrecj  15864  log2tlbndlog2  16082  sgmppw  16106  lgsval  16123  lgsfvalg  16124  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  gausslemma2dlem1f1o  16179  gausslemma2dlem4  16183  lgseisenlem2  16190  2lgslem1b  16208  vtxvalg  16257  iedgvalg  16258  edgvalg  16300  edgopval  16303  edgstruct  16305  vtxdgfifival  16532  wksfval  16563  trlsfvalg  16624  clwwlkg  16634  clwwlknonmpo  16669  eupthsg  16686  depindlem1  16747  pw1map  17025  subctctexmid  17030  nninffeq  17063  nnnninfex  17065  repiecele0  17075  repiecege0  17076  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  iswomni0  17101  dceqnconst  17110  dcapnconst  17111  nconstwlpolemgt0  17114