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

Theorem feq23d 6505
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 2826 . 2 (𝜑𝐹 = 𝐹)
2 feq23d.1 . 2 (𝜑𝐴 = 𝐶)
3 feq23d.2 . 2 (𝜑𝐵 = 𝐷)
41, 2, 3feq123d 6499 1 (𝜑 → (𝐹:𝐴𝐵𝐹:𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wf 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-fun 6353  df-fn 6354  df-f 6355
This theorem is referenced by:  nvof1o  7034  axdc4uz  13345  isacs  16915  isfunc  17127  funcres  17159  funcpropd  17163  estrcco  17373  funcestrcsetclem9  17391  fullestrcsetc  17394  fullsetcestrc  17409  1stfcl  17440  2ndfcl  17441  evlfcl  17465  curf1cl  17471  yonedalem3b  17522  intopsn  17856  mhmpropd  17953  pwssplit1  19754  evls1sca  20406  islindf  20875  rrxds  23914  wlkp1  27380  acunirnmpt  30322  fnpreimac  30334  cnmbfm  31410  elmrsubrn  32654  poimirlem3  34765  poimirlem28  34790  isrngod  35047  rngosn3  35073  isgrpda  35104  islfld  36068  tendofset  37764  tendoset  37765  mapfzcons  39181  diophrw  39224  refsum2cnlem1  41162  mgmhmpropd  43887  funcringcsetcALTV2lem9  44150  funcringcsetclem9ALTV  44173  aacllem  44737
  Copyright terms: Public domain W3C validator