Theorem fvmptd3 5612

Description: Deduction version of fvmpt 5596. (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 2319	. . 3 ⊢ Ⅎ𝑥𝐴
4		nfcv 2319	. . 3 ⊢ Ⅎ𝑥𝐶
5		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
6		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
7	3, 4, 5, 6	fvmptf 5611	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 411	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148   ↦ cmpt 4066  ‘cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226

This theorem is referenced by:  ofvalg  6095  fival  6972  inl11  7067  djuss  7072  ctmlemr  7110  ctssdclemn0  7112  ctssdc  7115  enumctlemm  7116  nninfisollemne  7132  nninfisol  7134  fodjum  7147  fodju0  7148  ismkvnex  7156  nninfwlporlemd  7173  nninfwlpoimlemg  7176  nninfwlpoimlemginf  7177  cc2lem  7268  xrnegiso  11273  summodclem3  11391  fsumf1o  11401  fsum3ser  11408  fsumadd  11417  sumsnf  11420  prodfdivap  11558  prodmodclem3  11586  prodmodclem2a  11587  fprodseq  11594  fprodf1o  11599  prodsnf  11603  fprodshft  11629  fprodrev  11630  eulerthlemh  12234  eulerthlemth  12235  phisum  12243  1arithlem2  12365  ennnfonelemjn  12406  ennnfonelemp1  12410  ctiunctlemfo  12443  nninfdclemf  12453  nninfdclemp1  12454  ptex  12719  divsfvalg  12754  plusffvalg  12787  grpidvalg  12798  issubm  12869  grpinvfvalg  12921  grpinvval  12922  grpsubfvalg  12924  grplactfval  12977  mulgfvalg  12991  issubg  13039  subgex  13042  isnsg  13068  mgpvalg  13139  srglmhm  13182  srgrmhm  13183  opprvalg  13247  reldvdsrsrg  13267  dvdsrvald  13268  isunitd  13281  invrfvald  13297  dvrfvald  13308  issubrg  13348  aprval  13378  aprap  13382  scaffvalg  13402  lsssetm  13450  lspfval  13481  lspval  13483  sraval  13529  rlmvalg  13546  ntrval  13750  clsval  13751  cnpval  13838  upxp  13912  uptx  13914  txlm  13919  cnmpt11  13923  cnmpt21  13931  ispsmet  13963  mopnval  14082  bdxmet  14141  cncfmptc  14222  cncfmptid  14223  addccncf  14226  negcncf  14228  ivthdec  14262  limcmpted  14272  cnmptlimc  14283  dvrecap  14317  dveflem  14327  dvef  14328  lgsval  14545  lgsfvalg  14546  lgsdir  14576  lgsdilem2  14577  lgsdi  14578  lgsne0  14579  lgseisenlem2  14591  subctctexmid  14891  nninffeq  14910  trilpolemclim  14925  trilpolemcl  14926  trilpolemisumle  14927  trilpolemeq1  14929  trilpolemlt1  14930  iswomni0  14940  dceqnconst  14949  dcapnconst  14950  nconstwlpolemgt0  14953