Theorem f1oeq3d 6797

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

Step	Hyp	Ref	Expression
1		f1oeq3d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq3 6790	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  –1-1-onto→wf1o 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  resdif  6821  f1osng  6841  f1oresrab  7099  fveqf1o  7277  isoini2  7314  oacomf1o  8529  mapsnf1o  8912  domss2  9100  dif1enlem  9120  dif1enlemOLD  9121  infn0  9251  wemapwe  9650  oef1o  9651  cnfcomlem  9652  cnfcom3  9657  cnfcom3clem  9658  infxpenc  9971  infxpenc2lem1  9972  infxpenc2  9975  ackbij2lem2  10192  hsmexlem1  10379  fsumss  15691  fsumcnv  15739  fprodss  15914  fprodcnv  15949  pwssnf1o  17461  catcisolem  18072  equivestrcsetc  18113  yoniso  18246  gsumpropd  18605  gsumpropd2lem  18606  xpsmnd  18704  xpsgrp  18991  ghmqusker  19219  gsumval3lem1  19835  gsumval3lem2  19836  gsumcom2  19905  xpsrngd  20088  xpsringd  20241  rngqiprngim  21214  coe1mul2lem2  22154  scmatrngiso  22423  m2cpmrngiso  22645  cncfcnvcn  24819  isismt  28461  usgrf1oedg  29134  wlkiswwlks2lem5  29803  clwwlkvbij  30042  eupthres  30144  eupthp1  30145  cycpmconjvlem  33098  tocyccntz  33101  idomsubr  33259  dimkerim  33623  prodeq12sdv  36206  cbvsumdavw2  36283  cbvproddavw2  36284  poimirlem4  37618  poimirlem9  37623  rngoisoval  37971  frlmsnic  42528  sge0f1o  46380  nnfoctbdj  46454  3f1oss1  47076  f1oresf1o  47291  grimidvtxedg  47885  ushggricedg  47927  uhgrimisgrgric  47931  isubgr3stgrlem3  47967  uptrlem1  49199  uptrar  49205  uptr2  49210  oduoppcciso  49555