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 17	. 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 17	. 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 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 1539  –1-1-onto→wf1o 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is referenced by:  f1oprswap  6871  f1oprg  6872  f1ossf1o  7127  cnfcom  9721  ackbij2lem2  10260  idffth  17950  ressffth  17955  symgval  19355  symg1bas  19375  symg2bas  19377  symgfixels  19419  symgfixelsi  19420  rnghmf1o  20419  rhmf1o  20458  mat1f1o  22431  ushgredgedg  29173  ushgredgedgloop  29175  trlreslem  29644  wlknwwlksnbij  29835  wwlksnextbij  29849  clwlknf1oclwwlkn  30030  eupth0  30160  eupthp1  30162  foresf1o  32450  f1ocnt  32734  indf1ofs  32782  gsumwrd2dccat  33000  symgcom  33033  cycpmcl  33066  cycpmconjslem2  33105  nsgqusf1o  33370  1arithidomlem2  33490  1arithidom  33491  dimkerim  33604  eulerpartgbij  34308  eulerpartlemn  34317  reprpmtf1o  34575  poimirlem16  37577  poimirlem17  37578  poimirlem19  37580  poimirlem20  37581  poimirlem28  37589  metakunt17  42156  wessf1ornlem  45123  disjf1o  45129  ssnnf1octb  45132  sge0fodjrnlem  46364  f1oresf1orab  47235  isgrim  47802  isubgrgrim  47831  isgrlim  47883  uspgrlim  47893  grlimgrtri  47897  grilcbri2  47905  swapf1f1o  48928  swapf2f1o  48929  swapf2f1oa  48930  swapf2f1oaALT  48931