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

Theorem feq23d 5938
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 2610 . 2 (𝜑𝐹 = 𝐹)
2 feq23d.1 . 2 (𝜑𝐴 = 𝐶)
3 feq23d.2 . 2 (𝜑𝐵 = 𝐷)
41, 2, 3feq123d 5932 1 (𝜑 → (𝐹:𝐴𝐵𝐹:𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wf 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-fun 5791  df-fn 5792  df-f 5793
This theorem is referenced by:  nvof1o  6413  axdc4uz  12602  isacs  16083  isfunc  16295  funcres  16327  funcpropd  16331  estrcco  16541  funcestrcsetclem9  16559  fullestrcsetc  16562  fullsetcestrc  16577  1stfcl  16608  2ndfcl  16609  evlfcl  16633  curf1cl  16639  yonedalem3b  16690  intopsn  17024  mhmpropd  17112  pwssplit1  18828  evls1sca  19457  islindf  19917  rrxds  22933  acunirnmpt  28634  cnmbfm  29445  elmrsubrn  30464  poimirlem3  32365  poimirlem28  32390  isrngod  32650  rngosn3  32676  isgrpda  32707  islfld  33150  tendofset  34847  tendoset  34848  mapfzcons  36080  diophrw  36123  refsum2cnlem1  38002  1wlkp1  40871  mgmhmpropd  41556  funcringcsetcALTV2lem9  41817  funcringcsetclem9ALTV  41840  aacllem  42298
  Copyright terms: Public domain W3C validator