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

Theorem f1oeq3d 6601
 Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
f1oeq3d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
f1oeq3d (𝜑 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))

Proof of Theorem f1oeq3d
StepHypRef Expression
1 f1oeq3d.1 . 2 (𝜑𝐴 = 𝐵)
2 f1oeq3 6595 . 2 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  –1-1-onto→wf1o 6343 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351 This theorem is referenced by:  resdif  6624  f1osng  6644  f1oresrab  6878  fveqf1o  7048  isoini2  7082  oacomf1o  8183  mapsnf1o  8495  domss2  8669  wemapwe  9153  oef1o  9154  cnfcomlem  9155  cnfcom3  9160  cnfcom3clem  9161  infxpenc  9438  infxpenc2lem1  9439  infxpenc2  9442  ackbij2lem2  9656  hsmexlem1  9842  fsumss  15080  fsumcnv  15126  fprodss  15300  fprodcnv  15335  pwssnf1o  16769  catcisolem  17364  equivestrcsetc  17400  yoniso  17533  gsumpropd  17886  gsumpropd2lem  17887  xpsmnd  17949  xpsgrp  18216  gsumval3lem1  19023  gsumval3lem2  19024  gsumcom2  19093  coe1mul2lem2  20431  scmatrngiso  21140  m2cpmrngiso  21361  cncfcnvcn  23528  isismt  26326  usgrf1oedg  26995  wlkiswwlks2lem5  27657  clwwlkvbij  27896  eupthres  27998  eupthp1  27999  cycpmconjvlem  30810  tocyccntz  30813  dimkerim  31053  poimirlem9  34978  rngoisoval  35327  frlmsnic  39331  sge0f1o  42887  nnfoctbdj  42961  f1oresf1o  43712  ushrisomgr  44225
 Copyright terms: Public domain W3C validator