Theorem f1oeq3d 6614

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 6608	. 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 1537  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  resdif  6637  f1osng  6657  f1oresrab  6891  fveqf1o  7060  isoini2  7094  oacomf1o  8193  mapsnf1o  8505  domss2  8678  wemapwe  9162  oef1o  9163  cnfcomlem  9164  cnfcom3  9169  cnfcom3clem  9170  infxpenc  9446  infxpenc2lem1  9447  infxpenc2  9450  ackbij2lem2  9664  hsmexlem1  9850  fsumss  15084  fsumcnv  15130  fprodss  15304  fprodcnv  15339  pwssnf1o  16773  catcisolem  17368  equivestrcsetc  17404  yoniso  17537  gsumpropd  17890  gsumpropd2lem  17891  xpsmnd  17953  xpsgrp  18220  gsumval3lem1  19027  gsumval3lem2  19028  gsumcom2  19097  coe1mul2lem2  20438  scmatrngiso  21147  m2cpmrngiso  21368  cncfcnvcn  23531  isismt  26322  usgrf1oedg  26991  wlkiswwlks2lem5  27653  clwwlkvbij  27894  eupthres  27996  eupthp1  27997  cycpmconjvlem  30785  tocyccntz  30788  dimkerim  31025  poimirlem9  34903  rngoisoval  35257  frlmsnic  39156  sge0f1o  42671  nnfoctbdj  42745  f1oresf1o  43496  ushrisomgr  44013