ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fvmptd3 GIF version

Theorem fvmptd3 5652
Description: Deduction version of fvmpt 5635. (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
StepHypRef Expression
1 fvmptd3.3 . 2 (𝜑𝐴𝐷)
2 fvmptd3.4 . 2 (𝜑𝐶𝑉)
3 nfcv 2336 . . 3 𝑥𝐴
4 nfcv 2336 . . 3 𝑥𝐶
5 fvmptd3.2 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
6 fvmptd3.1 . . 3 𝐹 = (𝑥𝐷𝐵)
73, 4, 5, 6fvmptf 5651 . 2 ((𝐴𝐷𝐶𝑉) → (𝐹𝐴) = 𝐶)
81, 2, 7syl2anc 411 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1364  wcel 2164  cmpt 4091  cfv 5255
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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2987  df-csb 3082  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-mpt 4093  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263
This theorem is referenced by:  ofvalg  6142  pw2f1odclem  6892  fival  7031  inl11  7126  djuss  7131  ctmlemr  7169  ctssdclemn0  7171  ctssdc  7174  enumctlemm  7175  nninfisollemne  7192  nninfisol  7194  fodjum  7207  fodju0  7208  ismkvnex  7216  nninfwlporlemd  7233  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  cc2lem  7328  seqf1oglem2  10594  seqf1og  10595  xrnegiso  11408  summodclem3  11526  fsumf1o  11536  fsum3ser  11543  fsumadd  11552  sumsnf  11555  prodfdivap  11693  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodf1o  11734  prodsnf  11738  fprodshft  11764  fprodrev  11765  nninfctlemfo  12180  eulerthlemh  12372  eulerthlemth  12373  phisum  12381  1arithlem2  12505  ennnfonelemjn  12562  ennnfonelemp1  12566  ctiunctlemfo  12599  nninfdclemf  12609  nninfdclemp1  12610  ptex  12878  divsfval  12914  divsfvalg  12915  plusffvalg  12948  grpidvalg  12959  issubm  13047  gsumfzz  13070  grpinvfvalg  13117  grpinvval  13118  grpsubfvalg  13120  grplactfval  13176  mulgfvalg  13194  issubg  13246  subgex  13249  isnsg  13275  conjghm  13349  conjnmz  13352  qusghm  13355  gsumfzconst  13414  gsumfzmhm2  13417  mgpvalg  13422  srglmhm  13492  srgrmhm  13493  ringlghm  13560  ringrghm  13561  opprvalg  13568  reldvdsrsrg  13591  dvdsrvald  13592  isunitd  13605  invrfvald  13621  dvrfvald  13632  issubrng  13698  issubrg  13720  rrgval  13761  aprval  13781  aprap  13785  scaffvalg  13805  lsssetm  13855  lspfval  13887  lspval  13889  sraval  13936  rlmvalg  13953  2idlvalg  14002  expghmap  14106  mulgghm2  14107  mulgrhm  14108  zrhvalg  14117  zrhmulg  14119  zlmval  14126  znval  14135  znzrhval  14146  ntrval  14289  clsval  14290  cnpval  14377  upxp  14451  uptx  14453  txlm  14458  cnmpt11  14462  cnmpt21  14470  ispsmet  14502  mopnval  14621  bdxmet  14680  cncfmptc  14775  cncfmptid  14776  addccncf  14779  negcncf  14784  ivthdec  14823  ivthreinc  14824  hovera  14826  hoverb  14827  hoverlt1  14828  hovergt0  14829  limcmpted  14842  cnmptlimc  14853  dvrecap  14892  dveflem  14905  dvef  14906  plyval  14911  plyrecj  14941  lgsval  15161  lgsfvalg  15162  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem1f1o  15217  gausslemma2dlem4  15221  lgseisenlem2  15228  2lgslem1b  15246  subctctexmid  15561  nninffeq  15580  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  iswomni0  15611  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624
  Copyright terms: Public domain W3C validator