Theorem fvmptd3 5609

Description: Deduction version of fvmpt 5593. (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 5608	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
8	1, 2, 7	syl2anc 411	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

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

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 4121  ax-pow 4174  ax-pr 4209

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 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224

This theorem is referenced by:  ofvalg  6091  fival  6968  inl11  7063  djuss  7068  ctmlemr  7106  ctssdclemn0  7108  ctssdc  7111  enumctlemm  7112  nninfisollemne  7128  nninfisol  7130  fodjum  7143  fodju0  7144  ismkvnex  7152  nninfwlporlemd  7169  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  cc2lem  7264  xrnegiso  11269  summodclem3  11387  fsumf1o  11397  fsum3ser  11404  fsumadd  11413  sumsnf  11416  prodfdivap  11554  prodmodclem3  11582  prodmodclem2a  11583  fprodseq  11590  fprodf1o  11595  prodsnf  11599  fprodshft  11625  fprodrev  11626  eulerthlemh  12230  eulerthlemth  12231  phisum  12239  1arithlem2  12361  ennnfonelemjn  12402  ennnfonelemp1  12406  ctiunctlemfo  12439  nninfdclemf  12449  nninfdclemp1  12450  ptex  12712  divsfvalg  12747  plusffvalg  12780  grpidvalg  12791  issubm  12862  grpinvfvalg  12914  grpinvval  12915  grpsubfvalg  12917  grplactfval  12970  mulgfvalg  12984  issubg  13031  subgex  13034  isnsg  13060  mgpvalg  13131  srglmhm  13174  srgrmhm  13175  opprvalg  13239  reldvdsrsrg  13259  dvdsrvald  13260  isunitd  13273  invrfvald  13289  dvrfvald  13300  issubrg  13340  aprval  13370  aprap  13374  scaffvalg  13394  ntrval  13580  clsval  13581  cnpval  13668  upxp  13742  uptx  13744  txlm  13749  cnmpt11  13753  cnmpt21  13761  ispsmet  13793  mopnval  13912  bdxmet  13971  cncfmptc  14052  cncfmptid  14053  addccncf  14056  negcncf  14058  ivthdec  14092  limcmpted  14102  cnmptlimc  14113  dvrecap  14147  dveflem  14157  dvef  14158  lgsval  14375  lgsfvalg  14376  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgseisenlem2  14421  subctctexmid  14720  nninffeq  14739  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  iswomni0  14769  dceqnconst  14777  dcapnconst  14778  nconstwlpolemgt0  14781