Theorem f1oeq1d 6843

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 6836	. 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 6560

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1orescnv  6863  f1osng  6889  f1ocoima  7323  f1ofvswap  7326  dif1en  9200  dif1enOLD  9202  cnfcomlem  9739  cnfcom2  9742  cnfcom3clem  9745  infxpenc  10058  infxpenc2lem2  10060  infxpenc2  10062  canthp1lem2  10693  pwfseqlem5  10703  pwfseq  10704  s2f1o  14955  s4f1o  14957  bitsf1ocnv  16481  yonffthlem  18327  grplactcnv  19061  eqgen  19199  znunithash  21583  tgpconncompeqg  24120  fcobijfs  32734  indf1o  32849  s2f1  32929  ccatws1f1o  32936  mgcf1o  32993  gsummpt2d  33052  gsumwrd2dccat  33070  subfacp1lem3  35187  subfacp1lem5  35189  ismrer1  37845  hvmap1o  41765  metakunt34  42239  3f1oss2  47088