Theorem f1oeq1d 6795

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 6788	. 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 6510

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1orescnv  6815  f1osng  6841  f1ocoima  7278  f1ofvswap  7281  dif1en  9124  dif1enOLD  9126  cnfcomlem  9652  cnfcom2  9655  cnfcom3clem  9658  infxpenc  9971  infxpenc2lem2  9973  infxpenc2  9975  canthp1lem2  10606  pwfseqlem5  10616  pwfseq  10617  s2f1o  14882  s4f1o  14884  bitsf1ocnv  16414  yonffthlem  18243  grplactcnv  18975  eqgen  19113  znunithash  21474  tgpconncompeqg  23999  fcobijfs  32646  indf1o  32787  s2f1  32866  ccatws1f1o  32873  mgcf1o  32929  gsummpt2d  32989  gsumwrd2dccat  33007  subfacp1lem3  35169  subfacp1lem5  35171  ismrer1  37832  hvmap1o  41757  3f1oss2  47077  idfu1stf1o  49088  imaidfu  49099  fucoppc  49399  lmdran  49660