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

Theorem feq23d 6711
Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)
Hypotheses
Ref Expression
feq23d.1 (𝜑𝐴 = 𝐶)
feq23d.2 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
feq23d (𝜑 → (𝐹:𝐴𝐵𝐹:𝐶𝐷))

Proof of Theorem feq23d
StepHypRef Expression
1 eqidd 2728 . 2 (𝜑𝐹 = 𝐹)
2 feq23d.1 . 2 (𝜑𝐴 = 𝐶)
3 feq23d.2 . 2 (𝜑𝐵 = 𝐷)
41, 2, 3feq123d 6705 1 (𝜑 → (𝐹:𝐴𝐵𝐹:𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wf 6538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-fun 6544  df-fn 6545  df-f 6546
This theorem is referenced by:  nvof1o  7283  axdc4uz  13973  isacs  17622  isfunc  17841  funcres  17873  funcpropd  17880  estrcco  18111  funcestrcsetclem9  18130  fullestrcsetc  18133  fullsetcestrc  18148  1stfcl  18179  2ndfcl  18180  evlfcl  18205  curf1cl  18211  yonedalem3b  18262  intopsn  18605  mgmhmpropd  18649  mhmpropd  18740  pwssplit1  20933  islindf  21733  evls1sca  22229  rrxds  25308  wlkp1  29482  acunirnmpt  32428  fnpreimac  32440  pwrssmgc  32709  cnmbfm  33819  elmrsubrn  35066  poimirlem3  37031  poimirlem28  37056  isrngod  37306  rngosn3  37332  isgrpda  37363  islfld  38471  tendofset  40168  tendoset  40169  mapfzcons  42058  diophrw  42101  refsum2cnlem1  44322  funcringcsetcALTV2lem9  47283  funcringcsetclem9ALTV  47306  aacllem  48157
  Copyright terms: Public domain W3C validator