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

Theorem feq23i 6730
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 6719 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐹:𝐴𝐵𝐹:𝐶𝐷))
41, 2, 3mp2an 692 1 (𝐹:𝐴𝐵𝐹:𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wf 6557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-fn 6564  df-f 6565
This theorem is referenced by:  ftpg  7176  hashf  14377  funcoppc  17920  cnextfval  24070  uhgr0  29090  lfgredgge2  29141  mbfmvolf  34268  eulerpartlemt  34373  ismgmOLD  37857  elghomOLD  37894  tendoset  40761  pwssplit4  43101  gricushgr  47886  uspgrlimlem2  47956  lincdifsn  48341
  Copyright terms: Public domain W3C validator