Theorem f1oeq3d 6607

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 6601	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  –1-1-onto→wf1o 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357

This theorem is referenced by:  resdif  6630  f1osng  6650  f1oresrab  6884  fveqf1o  7052  isoini2  7086  oacomf1o  8185  mapsnf1o  8497  domss2  8670  wemapwe  9154  oef1o  9155  cnfcomlem  9156  cnfcom3  9161  cnfcom3clem  9162  infxpenc  9438  infxpenc2lem1  9439  infxpenc2  9442  ackbij2lem2  9656  hsmexlem1  9842  fsumss  15076  fsumcnv  15122  fprodss  15296  fprodcnv  15331  pwssnf1o  16765  catcisolem  17360  equivestrcsetc  17396  yoniso  17529  gsumpropd  17882  gsumpropd2lem  17883  xpsmnd  17945  xpsgrp  18212  gsumval3lem1  19019  gsumval3lem2  19020  gsumcom2  19089  coe1mul2lem2  20430  scmatrngiso  21139  m2cpmrngiso  21360  cncfcnvcn  23523  isismt  26314  usgrf1oedg  26983  wlkiswwlks2lem5  27645  clwwlkvbij  27886  eupthres  27988  eupthp1  27989  cycpmconjvlem  30778  tocyccntz  30781  dimkerim  31018  poimirlem9  34895  rngoisoval  35249  frlmsnic  39142  sge0f1o  42657  nnfoctbdj  42731  f1oresf1o  43482  ushrisomgr  43999