Theorem f1oeq3d 6388

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  –1-1-onto→wf1o 6134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-in 3798  df-ss 3805  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142

This theorem is referenced by:  resdif  6411  f1osng  6431  f1oresrab  6659  fveqf1o  6829  isoini2  6861  oacomf1o  7929  mapsnf1o  8235  domss2  8407  wemapwe  8891  oef1o  8892  cnfcomlem  8893  cnfcom3  8898  cnfcom3clem  8899  infxpenc  9174  infxpenc2lem1  9175  infxpenc2  9178  ackbij2lem2  9397  hsmexlem1  9583  fsumss  14863  fsumcnv  14909  fprodss  15081  fprodcnv  15116  pwssnf1o  16544  catcisolem  17141  equivestrcsetc  17178  yoniso  17311  coe1mul2lem2  20034  usgrf1oedg  26553  wlkiswwlks2lem5  27222  clwwlkvbij  27515  clwwlkvbijOLD  27516  eupthresOLD  27618  eupthres  27619  eupthp1  27620  dimkerim  30441  poimirlem9  34039  sge0f1o  41516  nnfoctbdj  41590  f1oresf1o  42324  f1oresf1o2  42325  ushrisomgr  42747