Theorem f1oeq123d 6821

Description: Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)

Hypotheses

Ref	Expression
f1eq123d.1	⊢ (𝜑 → 𝐹 = 𝐺)
f1eq123d.2	⊢ (𝜑 → 𝐴 = 𝐵)
f1eq123d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
f1oeq123d	⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Proof of Theorem f1oeq123d

Step	Hyp	Ref	Expression
1		f1eq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2		f1oeq1 6815	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
3	1, 2	syl 18	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1oeq2 6816	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
6	4, 5	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1oeq3 6817	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 18	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 308	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  –1-1-onto→wf1o 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is used by:  f1oprswap  6873  f1oprg  6874  f1ossf1o  7132  cnfcom  9706  ackbij2lem2  10322  idffth  18117  ressffth  18122  symgval  19592  symg1bas  19612  symg2bas  19614  symgfixels  19655  symgfixelsi  19656  rnghmf1o  20689  rhmf1o  20734  mat1f1o  22800  ushgredgedg  29817  ushgredgedgloop  29819  trlreslem  30289  wlknwwlksnbij  30484  wwlksnextbij  30498  clwlknf1oclwwlkn  30682  eupth0  30822  eupthp1  30824  foresf1o  33149  f1ocnt  33440  indf1ofs  33481  gsumwrd2dccat  33687  symgcom  33692  cycpmcl  33725  cycpmconjslem2  33764  nsgqusf1o  34015  1arithidomlem2  34116  1arithidom  34117  dimkerim  34307  eulerpartgbij  35052  eulerpartlemn  35061  reprpmtf1o  35303  poimirlem16  38661  poimirlem17  38662  poimirlem19  38664  poimirlem20  38665  poimirlem28  38673  wessf1ornlem  46307  disjf1o  46313  ssnnf1octb  46316  sge0fodjrnlem  47533  f1oresf1orab  48466  isgrim  49087  isubgrgrim  49134  isgrlim  49187  uspgrlim  49197  grlimedgclnbgr  49200  grlimgrtri  49208  grilcbri2  49216  gpg5grlim  49298  swapf1f1o  50504  swapf2f1o  50505  swapf2f1oa  50506  swapf2f1oaALT  50507  fucoppc  50652