Theorem fvmptd3 5727

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200   ↦ cmpt 4144  ‘cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-csb 3125  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-iota 5277  df-fun 5319  df-fv 5325

This theorem is referenced by:  ofvalg  6226  pw2f1odclem  6991  fival  7133  inl11  7228  djuss  7233  ctmlemr  7271  ctssdclemn0  7273  ctssdc  7276  enumctlemm  7277  nninfisollemne  7294  nninfisol  7296  fodjum  7309  fodju0  7310  ismkvnex  7318  nninfwlporlemd  7335  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  cc2lem  7448  seqf1oglem2  10737  seqf1og  10738  lswwrd  11113  swrdfv  11180  swrdswrd  11232  xrnegiso  11768  summodclem3  11886  fsumf1o  11896  fsum3ser  11903  fsumadd  11912  sumsnf  11915  prodfdivap  12053  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodf1o  12094  prodsnf  12098  fprodshft  12124  fprodrev  12125  nninfctlemfo  12556  eulerthlemh  12748  eulerthlemth  12749  phisum  12758  1arithlem2  12882  ennnfonelemjn  12968  ennnfonelemp1  12972  ctiunctlemfo  13005  nninfdclemf  13015  nninfdclemp1  13016  ptex  13292  prdsplusgfval  13312  prdsmulrfval  13314  divsfval  13356  divsfvalg  13357  plusffvalg  13390  grpidvalg  13401  issubm  13500  gsumfzz  13523  grpinvfvalg  13570  grpinvval  13571  grpsubfvalg  13573  grplactfval  13629  prdsinvlem  13636  mulgfvalg  13653  issubg  13705  subgex  13708  isnsg  13734  conjghm  13808  conjnmz  13811  qusghm  13814  gsumfzconst  13873  gsumfzmhm2  13876  mgpvalg  13881  srglmhm  13951  srgrmhm  13952  ringlghm  14019  ringrghm  14020  opprvalg  14027  reldvdsrsrg  14050  dvdsrvald  14051  isunitd  14064  invrfvald  14080  dvrfvald  14091  issubrng  14157  issubrg  14179  rrgval  14220  aprval  14240  aprap  14244  scaffvalg  14264  lsssetm  14314  lspfval  14346  lspval  14348  sraval  14395  rlmvalg  14412  2idlvalg  14461  expghmap  14565  mulgghm2  14566  mulgrhm  14567  zrhvalg  14576  zrhmulg  14578  zlmval  14585  znval  14594  znzrhval  14605  ntrval  14778  clsval  14779  cnpval  14866  upxp  14940  uptx  14942  txlm  14947  cnmpt11  14951  cnmpt21  14959  ispsmet  14991  mopnval  15110  bdxmet  15169  cncfmptc  15264  cncfmptid  15265  addccncf  15268  negcncf  15273  ivthdec  15312  ivthreinc  15313  hovera  15315  hoverb  15316  hoverlt1  15317  hovergt0  15318  limcmpted  15331  cnmptlimc  15342  dvrecap  15381  dveflem  15394  dvef  15395  plyval  15400  plycoeid3  15425  plyrecj  15431  sgmppw  15660  lgsval  15677  lgsfvalg  15678  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  gausslemma2dlem1f1o  15733  gausslemma2dlem4  15737  lgseisenlem2  15744  2lgslem1b  15762  vtxvalg  15811  iedgvalg  15812  edgvalg  15854  edgopval  15856  edgstruct  15858  wksfval  16028  2omap  16318  pw1map  16320  subctctexmid  16325  nninffeq  16345  nnnninfex  16347  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  iswomni0  16378  dceqnconst  16387  dcapnconst  16388  nconstwlpolemgt0  16391