Theorem f1oeq123d 6850

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 6844	. . 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 6845	. . 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 6846	. . 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 6568

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3483  df-dif 3969  df-un 3971  df-ss 3983  df-nul 4343  df-if 4535  df-sn 4635  df-pr 4637  df-op 4641  df-br 5152  df-opab 5214  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576

This theorem is referenced by:  f1oprswap  6900  f1oprg  6901  f1ossf1o  7155  cnfcom  9747  ackbij2lem2  10286  idffth  17996  ressffth  18001  symgval  19412  symg1bas  19432  symg2bas  19434  symgfixels  19476  symgfixelsi  19477  rnghmf1o  20478  rhmf1o  20517  mat1f1o  22509  ushgredgedg  29272  ushgredgedgloop  29274  trlreslem  29743  wlknwwlksnbij  29934  wwlksnextbij  29948  clwlknf1oclwwlkn  30129  eupth0  30259  eupthp1  30261  foresf1o  32547  f1ocnt  32824  indf1ofs  32869  gsumwrd2dccat  33085  symgcom  33118  cycpmcl  33151  cycpmconjslem2  33190  nsgqusf1o  33456  1arithidomlem2  33576  1arithidom  33577  dimkerim  33687  eulerpartgbij  34368  eulerpartlemn  34377  reprpmtf1o  34634  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem28  37649  metakunt17  42217  wessf1ornlem  45157  disjf1o  45163  ssnnf1octb  45166  sge0fodjrnlem  46400  f1oresf1orab  47267  isgrim  47834  isubgrgrim  47863  isgrlim  47915  uspgrlim  47925  grlimgrtri  47929  grilcbri2  47937