Theorem f1oeq3d 6697

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 6690	. 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 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  resdif  6720  f1osng  6740  f1oresrab  6981  fveqf1o  7155  isoini2  7190  oacomf1o  8358  mapsnf1o  8685  domss2  8872  dif1enlem  8905  wemapwe  9385  oef1o  9386  cnfcomlem  9387  cnfcom3  9392  cnfcom3clem  9393  infxpenc  9705  infxpenc2lem1  9706  infxpenc2  9709  ackbij2lem2  9927  hsmexlem1  10113  fsumss  15365  fsumcnv  15413  fprodss  15586  fprodcnv  15621  pwssnf1o  17126  catcisolem  17741  equivestrcsetc  17785  yoniso  17919  gsumpropd  18277  gsumpropd2lem  18278  xpsmnd  18340  xpsgrp  18609  gsumval3lem1  19421  gsumval3lem2  19422  gsumcom2  19491  coe1mul2lem2  21349  scmatrngiso  21593  m2cpmrngiso  21815  cncfcnvcn  23994  isismt  26799  usgrf1oedg  27477  wlkiswwlks2lem5  28139  clwwlkvbij  28378  eupthres  28480  eupthp1  28481  cycpmconjvlem  31310  tocyccntz  31313  dimkerim  31610  poimirlem4  35708  poimirlem9  35713  rngoisoval  36062  frlmsnic  40188  sge0f1o  43810  nnfoctbdj  43884  f1oresf1o  44669  ushrisomgr  45181