Theorem fvmptd3 5696

Description: Deduction version of fvmpt 5679. (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 2350	. . 3 |- F/_ x A
4		nfcv 2350	. . 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 5695	. 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 1373   e. wcel 2178   |-> cmpt 4121   ` cfv 5290

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-sbc 3006  df-csb 3102  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-iota 5251  df-fun 5292  df-fv 5298

This theorem is referenced by:  ofvalg  6191  pw2f1odclem  6956  fival  7098  inl11  7193  djuss  7198  ctmlemr  7236  ctssdclemn0  7238  ctssdc  7241  enumctlemm  7242  nninfisollemne  7259  nninfisol  7261  fodjum  7274  fodju0  7275  ismkvnex  7283  nninfwlporlemd  7300  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  cc2lem  7413  seqf1oglem2  10702  seqf1og  10703  lswwrd  11077  swrdfv  11144  swrdswrd  11196  xrnegiso  11688  summodclem3  11806  fsumf1o  11816  fsum3ser  11823  fsumadd  11832  sumsnf  11835  prodfdivap  11973  prodmodclem3  12001  prodmodclem2a  12002  fprodseq  12009  fprodf1o  12014  prodsnf  12018  fprodshft  12044  fprodrev  12045  nninfctlemfo  12476  eulerthlemh  12668  eulerthlemth  12669  phisum  12678  1arithlem2  12802  ennnfonelemjn  12888  ennnfonelemp1  12892  ctiunctlemfo  12925  nninfdclemf  12935  nninfdclemp1  12936  ptex  13211  prdsplusgfval  13231  prdsmulrfval  13233  divsfval  13275  divsfvalg  13276  plusffvalg  13309  grpidvalg  13320  issubm  13419  gsumfzz  13442  grpinvfvalg  13489  grpinvval  13490  grpsubfvalg  13492  grplactfval  13548  prdsinvlem  13555  mulgfvalg  13572  issubg  13624  subgex  13627  isnsg  13653  conjghm  13727  conjnmz  13730  qusghm  13733  gsumfzconst  13792  gsumfzmhm2  13795  mgpvalg  13800  srglmhm  13870  srgrmhm  13871  ringlghm  13938  ringrghm  13939  opprvalg  13946  reldvdsrsrg  13969  dvdsrvald  13970  isunitd  13983  invrfvald  13999  dvrfvald  14010  issubrng  14076  issubrg  14098  rrgval  14139  aprval  14159  aprap  14163  scaffvalg  14183  lsssetm  14233  lspfval  14265  lspval  14267  sraval  14314  rlmvalg  14331  2idlvalg  14380  expghmap  14484  mulgghm2  14485  mulgrhm  14486  zrhvalg  14495  zrhmulg  14497  zlmval  14504  znval  14513  znzrhval  14524  ntrval  14697  clsval  14698  cnpval  14785  upxp  14859  uptx  14861  txlm  14866  cnmpt11  14870  cnmpt21  14878  ispsmet  14910  mopnval  15029  bdxmet  15088  cncfmptc  15183  cncfmptid  15184  addccncf  15187  negcncf  15192  ivthdec  15231  ivthreinc  15232  hovera  15234  hoverb  15235  hoverlt1  15236  hovergt0  15237  limcmpted  15250  cnmptlimc  15261  dvrecap  15300  dveflem  15313  dvef  15314  plyval  15319  plycoeid3  15344  plyrecj  15350  sgmppw  15579  lgsval  15596  lgsfvalg  15597  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  gausslemma2dlem1f1o  15652  gausslemma2dlem4  15656  lgseisenlem2  15663  2lgslem1b  15681  vtxvalg  15730  iedgvalg  15731  edgvalg  15771  edgopval  15773  edgstruct  15775  2omap  16132  pw1map  16134  subctctexmid  16139  nninffeq  16159  nnnninfex  16161  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  iswomni0  16192  dceqnconst  16201  dcapnconst  16202  nconstwlpolemgt0  16205