Theorem f1oeq123d 6801

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 6795	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶))
4		f1eq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
5		f1oeq2 6796	. . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
6	4, 5	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶))
7		f1eq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
8		f1oeq3 6797	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 305	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  –1-1-onto→wf1o 6518

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3412  df-v 3457  df-dif 3925  df-un 3927  df-ss 3939  df-nul 4305  df-if 4497  df-sn 4598  df-pr 4600  df-op 4604  df-br 5116  df-opab 5178  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-fun 6521  df-fn 6522  df-f 6523  df-f1 6524  df-fo 6525  df-f1o 6526

This theorem is referenced by:  f1oprswap  6851  f1oprg  6852  f1ossf1o  7107  cnfcom  9671  ackbij2lem2  10210  idffth  17903  ressffth  17908  symgval  19307  symg1bas  19327  symg2bas  19329  symgfixels  19370  symgfixelsi  19371  rnghmf1o  20367  rhmf1o  20406  mat1f1o  22371  ushgredgedg  29163  ushgredgedgloop  29165  trlreslem  29634  wlknwwlksnbij  29825  wwlksnextbij  29839  clwlknf1oclwwlkn  30020  eupth0  30150  eupthp1  30152  foresf1o  32440  f1ocnt  32733  indf1ofs  32797  gsumwrd2dccat  33015  symgcom  33048  cycpmcl  33081  cycpmconjslem2  33120  nsgqusf1o  33395  1arithidomlem2  33515  1arithidom  33516  dimkerim  33631  eulerpartgbij  34371  eulerpartlemn  34380  reprpmtf1o  34625  poimirlem16  37627  poimirlem17  37628  poimirlem19  37630  poimirlem20  37631  poimirlem28  37639  wessf1ornlem  45151  disjf1o  45157  ssnnf1octb  45160  sge0fodjrnlem  46387  f1oresf1orab  47260  isgrim  47837  isubgrgrim  47884  isgrlim  47936  uspgrlim  47946  grlimgrtri  47950  grilcbri2  47958  swapf1f1o  49176  swapf2f1o  49177  swapf2f1oa  49178  swapf2f1oaALT  49179