Theorem f1oeq1d 6823

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 6816	. 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 1539  –1-1-onto→wf1o 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is referenced by:  f1orescnv  6843  f1osng  6869  f1ocoima  7305  f1ofvswap  7308  dif1en  9182  dif1enOLD  9184  cnfcomlem  9721  cnfcom2  9724  cnfcom3clem  9727  infxpenc  10040  infxpenc2lem2  10042  infxpenc2  10044  canthp1lem2  10675  pwfseqlem5  10685  pwfseq  10686  s2f1o  14937  s4f1o  14939  bitsf1ocnv  16463  yonffthlem  18297  grplactcnv  19030  eqgen  19168  znunithash  21537  tgpconncompeqg  24066  fcobijfs  32669  indf1o  32789  s2f1  32869  ccatws1f1o  32876  mgcf1o  32932  gsummpt2d  32991  gsumwrd2dccat  33009  subfacp1lem3  35146  subfacp1lem5  35148  ismrer1  37804  hvmap1o  41724  metakunt34  42198  3f1oss2  47046