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

Theorem f1oeq3d 6606
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 6600 . 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 207   = wceq 1528  1-1-ontowf1o 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356
This theorem is referenced by:  resdif  6629  f1osng  6649  f1oresrab  6882  fveqf1o  7049  isoini2  7081  oacomf1o  8181  mapsnf1o  8492  domss2  8665  wemapwe  9149  oef1o  9150  cnfcomlem  9151  cnfcom3  9156  cnfcom3clem  9157  infxpenc  9433  infxpenc2lem1  9434  infxpenc2  9437  ackbij2lem2  9651  hsmexlem1  9837  fsumss  15072  fsumcnv  15118  fprodss  15292  fprodcnv  15327  pwssnf1o  16761  catcisolem  17356  equivestrcsetc  17392  yoniso  17525  gsumpropd  17878  gsumpropd2lem  17879  xpsmnd  17941  xpsgrp  18158  gsumval3lem1  18956  gsumval3lem2  18957  gsumcom2  19026  coe1mul2lem2  20366  scmatrngiso  21075  m2cpmrngiso  21296  cncfcnvcn  23458  isismt  26248  usgrf1oedg  26917  wlkiswwlks2lem5  27579  clwwlkvbij  27820  eupthres  27922  eupthp1  27923  cycpmconjvlem  30711  tocyccntz  30714  dimkerim  30923  poimirlem9  34783  rngoisoval  35138  frlmsnic  39029  sge0f1o  42545  nnfoctbdj  42619  f1oresf1o  43370  ushrisomgr  43853
  Copyright terms: Public domain W3C validator