Theorem f1oeq1d 6798

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
f1oeq1d	⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Proof of Theorem f1oeq1d

Step	Hyp	Ref	Expression
1		f1oeq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1oeq1 6791	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  –1-1-onto→wf1o 6513

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1orescnv  6818  f1osng  6844  f1ocoima  7281  f1ofvswap  7284  dif1en  9130  dif1enOLD  9132  cnfcomlem  9659  cnfcom2  9662  cnfcom3clem  9665  infxpenc  9978  infxpenc2lem2  9980  infxpenc2  9982  canthp1lem2  10613  pwfseqlem5  10623  pwfseq  10624  s2f1o  14889  s4f1o  14891  bitsf1ocnv  16421  yonffthlem  18250  grplactcnv  18982  eqgen  19120  znunithash  21481  tgpconncompeqg  24006  fcobijfs  32653  indf1o  32794  s2f1  32873  ccatws1f1o  32880  mgcf1o  32936  gsummpt2d  32996  gsumwrd2dccat  33014  subfacp1lem3  35176  subfacp1lem5  35178  ismrer1  37839  hvmap1o  41764  3f1oss2  47081  idfu1stf1o  49092  imaidfu  49103  fucoppc  49403  lmdran  49664