MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq23i Structured version   Visualization version   GIF version

Theorem feq23i 6731
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
feq23i.1 𝐴 = 𝐶
feq23i.2 𝐵 = 𝐷
Assertion
Ref Expression
feq23i (𝐹:𝐴𝐵𝐹:𝐶𝐷)

Proof of Theorem feq23i
StepHypRef Expression
1 feq23i.1 . 2 𝐴 = 𝐶
2 feq23i.2 . 2 𝐵 = 𝐷
3 feq23 6720 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐹:𝐴𝐵𝐹:𝐶𝐷))
41, 2, 3mp2an 692 1 (𝐹:𝐴𝐵𝐹:𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1537  wf 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-fn 6566  df-f 6567
This theorem is referenced by:  ftpg  7176  hashf  14374  funcoppc  17926  cnextfval  24086  uhgr0  29105  lfgredgge2  29156  mbfmvolf  34248  eulerpartlemt  34353  ismgmOLD  37837  elghomOLD  37874  tendoset  40742  pwssplit4  43078  gricushgr  47824  uspgrlimlem2  47892  lincdifsn  48270
  Copyright terms: Public domain W3C validator