Theorem fvmptd3 5740

Description: Deduction version of fvmpt 5723. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
fvmptd3.1	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmptd3.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptd3.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd3.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd3	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd3

Step	Hyp	Ref	Expression
1		fvmptd3.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
2		fvmptd3.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		nfcv 2374	. . 3 ⊢ Ⅎ𝑥𝐴
4		nfcv 2374	. . 3 ⊢ Ⅎ𝑥𝐶
5		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
6		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
7	3, 4, 5, 6	fvmptf 5739	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 411	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202   ↦ cmpt 4150  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-csb 3128  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334

This theorem is referenced by:  ofvalg  6244  pw2f1odclem  7019  fival  7168  inl11  7263  djuss  7268  ctmlemr  7306  ctssdclemn0  7308  ctssdc  7311  enumctlemm  7312  nninfisollemne  7329  nninfisol  7331  fodjum  7344  fodju0  7345  ismkvnex  7353  nninfwlporlemd  7370  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  cc2lem  7484  seqf1oglem2  10781  seqf1og  10782  lswwrd  11159  swrdfv  11233  swrdswrd  11285  xrnegiso  11822  summodclem3  11940  fsumf1o  11950  fsum3ser  11957  fsumadd  11966  sumsnf  11969  prodfdivap  12107  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodf1o  12148  prodsnf  12152  fprodshft  12178  fprodrev  12179  nninfctlemfo  12610  eulerthlemh  12802  eulerthlemth  12803  phisum  12812  1arithlem2  12936  ennnfonelemjn  13022  ennnfonelemp1  13026  ctiunctlemfo  13059  nninfdclemf  13069  nninfdclemp1  13070  ptex  13346  prdsplusgfval  13366  prdsmulrfval  13368  divsfval  13410  divsfvalg  13411  plusffvalg  13444  grpidvalg  13455  issubm  13554  gsumfzz  13577  grpinvfvalg  13624  grpinvval  13625  grpsubfvalg  13627  grplactfval  13683  prdsinvlem  13690  mulgfvalg  13707  issubg  13759  subgex  13762  isnsg  13788  conjghm  13862  conjnmz  13865  qusghm  13868  gsumfzconst  13927  gsumfzmhm2  13930  mgpvalg  13935  srglmhm  14005  srgrmhm  14006  ringlghm  14073  ringrghm  14074  opprvalg  14081  dvdsrvald  14106  isunitd  14119  invrfvald  14135  dvrfvald  14146  issubrng  14212  issubrg  14234  rrgval  14275  aprval  14295  aprap  14299  scaffvalg  14319  lsssetm  14369  lspfval  14401  lspval  14403  sraval  14450  rlmvalg  14467  2idlvalg  14516  expghmap  14620  mulgghm2  14621  mulgrhm  14622  zrhvalg  14631  zrhmulg  14633  zlmval  14640  znval  14649  znzrhval  14660  ntrval  14833  clsval  14834  cnpval  14921  upxp  14995  uptx  14997  txlm  15002  cnmpt11  15006  cnmpt21  15014  ispsmet  15046  mopnval  15165  bdxmet  15224  cncfmptc  15319  cncfmptid  15320  addccncf  15323  negcncf  15328  ivthdec  15367  ivthreinc  15368  hovera  15370  hoverb  15371  hoverlt1  15372  hovergt0  15373  limcmpted  15386  cnmptlimc  15397  dvrecap  15436  dveflem  15449  dvef  15450  plyval  15455  plycoeid3  15480  plyrecj  15486  sgmppw  15715  lgsval  15732  lgsfvalg  15733  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  lgseisenlem2  15799  2lgslem1b  15817  vtxvalg  15866  iedgvalg  15867  edgvalg  15909  edgopval  15912  edgstruct  15914  vtxdgfifival  16141  wksfval  16172  trlsfvalg  16233  clwwlkg  16243  clwwlknonmpo  16278  eupthsg  16295  2omap  16594  pw1map  16596  subctctexmid  16601  nninffeq  16622  nnnninfex  16624  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  iswomni0  16655  dceqnconst  16664  dcapnconst  16665  nconstwlpolemgt0  16668  gsumgfsumlem  16683