Theorem f1oeq123d 6612

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 6606	. . 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 6607	. . 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 6608	. . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
9	7, 8	syl 17	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
10	3, 6, 9	3bitrd 308	1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  –1-1-onto→wf1o 6338

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346

This theorem is referenced by:  f1oprswap  6661  f1oprg  6662  f1ossf1o  6900  cnfcom  9236  ackbij2lem2  9740  idffth  17308  ressffth  17313  symgval  18615  symg1bas  18637  symg2bas  18639  symgfixels  18680  symgfixelsi  18681  rhmf1o  19606  mat1f1o  21229  ushgredgedg  27171  ushgredgedgloop  27173  trlreslem  27641  wlknwwlksnbij  27826  wwlksnextbij  27840  clwlknf1oclwwlkn  28021  eupth0  28151  eupthp1  28153  foresf1o  30424  f1ocnt  30698  symgcom  30929  cycpmcl  30960  cycpmconjslem2  30999  nsgqusf1o  31173  dimkerim  31280  indf1ofs  31564  eulerpartgbij  31909  eulerpartlemn  31918  reprpmtf1o  32176  poimirlem16  35416  poimirlem17  35417  poimirlem19  35419  poimirlem20  35420  poimirlem28  35428  metakunt17  39732  wessf1ornlem  42260  disjf1o  42267  ssnnf1octb  42271  sge0fodjrnlem  43496  f1oresf1orab  44314  isomgr  44809  rnghmf1o  44995