Theorem f1oeq123d 6776

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 6770	. . 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 6771	. . 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 6772	. . 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 1542  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1oprswap  6827  f1oprg  6828  f1ossf1o  7083  cnfcom  9621  ackbij2lem2  10161  idffth  17871  ressffth  17876  symgval  19312  symg1bas  19332  symg2bas  19334  symgfixels  19375  symgfixelsi  19376  rnghmf1o  20400  rhmf1o  20438  mat1f1o  22434  ushgredgedg  29314  ushgredgedgloop  29316  trlreslem  29783  wlknwwlksnbij  29973  wwlksnextbij  29987  clwlknf1oclwwlkn  30171  eupth0  30301  eupthp1  30303  foresf1o  32591  f1ocnt  32891  indf1ofs  32959  gsumwrd2dccat  33172  symgcom  33177  cycpmcl  33210  cycpmconjslem2  33249  nsgqusf1o  33509  1arithidomlem2  33629  1arithidom  33630  dimkerim  33805  eulerpartgbij  34550  eulerpartlemn  34559  reprpmtf1o  34804  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem28  37899  wessf1ornlem  45544  disjf1o  45550  ssnnf1octb  45553  sge0fodjrnlem  46774  f1oresf1orab  47649  isgrim  48242  isubgrgrim  48289  isgrlim  48342  uspgrlim  48352  grlimedgclnbgr  48355  grlimgrtri  48363  grilcbri2  48371  gpg5grlim  48453  swapf1f1o  49634  swapf2f1o  49635  swapf2f1oa  49636  swapf2f1oaALT  49637  fucoppc  49769