Theorem f1oeq3d 6829

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  –1-1-onto→wf1o 6541

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549

This theorem is referenced by:  resdif  6853  f1osng  6873  f1oresrab  7126  fveqf1o  7303  isoini2  7338  oacomf1o  8567  mapsnf1o  8935  domss2  9138  dif1enlem  9158  dif1enlemOLD  9159  infn0  9309  wemapwe  9694  oef1o  9695  cnfcomlem  9696  cnfcom3  9701  cnfcom3clem  9702  infxpenc  10015  infxpenc2lem1  10016  infxpenc2  10019  ackbij2lem2  10237  hsmexlem1  10423  fsumss  15675  fsumcnv  15723  fprodss  15896  fprodcnv  15931  pwssnf1o  17448  catcisolem  18064  equivestrcsetc  18108  yoniso  18242  gsumpropd  18603  gsumpropd2lem  18604  xpsmnd  18699  xpsgrp  18978  gsumval3lem1  19814  gsumval3lem2  19815  gsumcom2  19884  xpsrngd  20073  xpsringd  20220  rngqiprngim  21063  coe1mul2lem2  22010  scmatrngiso  22258  m2cpmrngiso  22480  cncfcnvcn  24666  isismt  28052  usgrf1oedg  28731  wlkiswwlks2lem5  29394  clwwlkvbij  29633  eupthres  29735  eupthp1  29736  cycpmconjvlem  32570  tocyccntz  32573  ghmqusker  32806  dimkerim  33000  poimirlem4  36795  poimirlem9  36800  rngoisoval  37148  frlmsnic  41412  sge0f1o  45396  nnfoctbdj  45470  f1oresf1o  46296  ushrisomgr  46807