Theorem f1oeq123d 6762

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 6756	. . 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 6757	. . 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 6758	. . 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 6485

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1oprswap  6812  f1oprg  6813  f1ossf1o  7066  cnfcom  9615  ackbij2lem2  10152  idffth  17861  ressffth  17866  symgval  19269  symg1bas  19289  symg2bas  19291  symgfixels  19332  symgfixelsi  19333  rnghmf1o  20356  rhmf1o  20395  mat1f1o  22382  ushgredgedg  29193  ushgredgedgloop  29195  trlreslem  29662  wlknwwlksnbij  29852  wwlksnextbij  29866  clwlknf1oclwwlkn  30047  eupth0  30177  eupthp1  30179  foresf1o  32467  f1ocnt  32764  indf1ofs  32828  gsumwrd2dccat  33039  symgcom  33044  cycpmcl  33077  cycpmconjslem2  33116  nsgqusf1o  33372  1arithidomlem2  33492  1arithidom  33493  dimkerim  33613  eulerpartgbij  34359  eulerpartlemn  34368  reprpmtf1o  34613  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem28  37647  wessf1ornlem  45183  disjf1o  45189  ssnnf1octb  45192  sge0fodjrnlem  46417  f1oresf1orab  47293  isgrim  47886  isubgrgrim  47933  isgrlim  47986  uspgrlim  47996  grlimedgclnbgr  47999  grlimgrtri  48007  grilcbri2  48015  gpg5grlim  48097  swapf1f1o  49280  swapf2f1o  49281  swapf2f1oa  49282  swapf2f1oaALT  49283  fucoppc  49415