Theorem f1oeq1d 6837

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 6830	. 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 1533  –1-1-onto→wf1o 6550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5151  df-opab 5213  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558

This theorem is referenced by:  f1orescnv  6857  f1osng  6883  f1ofvswap  7319  dif1en  9189  dif1enOLD  9191  cnfcomlem  9728  cnfcom2  9731  cnfcom3clem  9734  infxpenc  10047  infxpenc2lem2  10049  infxpenc2  10051  canthp1lem2  10682  pwfseqlem5  10692  pwfseq  10693  s2f1o  14905  s4f1o  14907  bitsf1ocnv  16424  yonffthlem  18279  grplactcnv  19004  eqgen  19141  znunithash  21503  tgpconncompeqg  24034  fcobijfs  32523  s2f1  32686  mgcf1o  32748  gsummpt2d  32781  indf1o  33648  subfacp1lem3  34797  subfacp1lem5  34799  ismrer1  37316  hvmap1o  41240  metakunt34  41694