Theorem f1oeq1d 6762

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1orescnv  6782  f1osng  6809  f1ocoima  7247  f1ofvswap  7250  dif1en  9086  cnfcomlem  9611  cnfcom2  9614  cnfcom3clem  9617  infxpenc  9931  infxpenc2lem2  9933  infxpenc2  9935  canthp1lem2  10567  pwfseqlem5  10577  pwfseq  10578  s2f1o  14869  s4f1o  14871  bitsf1ocnv  16404  yonffthlem  18239  grplactcnv  19010  eqgen  19147  znunithash  21539  tgpconncompeqg  24095  fcobijfs  32813  fcobijfs2  32814  indf1o  32943  s2f1  33024  ccatws1f1o  33030  mgcf1o  33082  gsummpt2d  33130  gsumwrd2dccat  33159  subfacp1lem3  35410  subfacp1lem5  35412  ismrer1  38205  hvmap1o  42255  3f1oss2  47539  idfu1stf1o  49589  imaidfu  49600  fucoppc  49900  lmdran  50161