Theorem f1oeq1d 6777

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 6770	. 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 1542  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1orescnv  6797  f1osng  6824  f1ocoima  7259  f1ofvswap  7262  dif1en  9098  cnfcomlem  9620  cnfcom2  9623  cnfcom3clem  9626  infxpenc  9940  infxpenc2lem2  9942  infxpenc2  9944  canthp1lem2  10576  pwfseqlem5  10586  pwfseq  10587  s2f1o  14851  s4f1o  14853  bitsf1ocnv  16383  yonffthlem  18217  grplactcnv  18985  eqgen  19122  znunithash  21531  tgpconncompeqg  24068  fcobijfs  32811  fcobijfs2  32812  indf1o  32957  s2f1  33038  ccatws1f1o  33044  mgcf1o  33096  gsummpt2d  33143  gsumwrd2dccat  33172  subfacp1lem3  35398  subfacp1lem5  35400  ismrer1  38089  hvmap1o  42139  3f1oss2  47436  idfu1stf1o  49458  imaidfu  49469  fucoppc  49769  lmdran  50030