Theorem f1oeq2 3685

Description: Equality theorem for one-to-one onto functions.

Assertion

Ref	Expression
f1oeq2	|- (A = B -> (F:A-1-1-onto->C <-> F:B-1-1-onto->C))

Proof of Theorem f1oeq2

Step	Hyp	Ref	Expression
1		f1eq2 3661	. . 3 |- (A = B -> (F:A-1-1->C <-> F:B-1-1->C))
2		foeq2 3669	. . 3 |- (A = B -> (F:A-onto->C <-> F:B-onto->C))
3	1, 2	anbi12d 628	. 2 |- (A = B -> ((F:A-1-1->C /\ F:A-onto->C) <-> (F:B-1-1->C /\ F:B-onto->C)))
4		df-f1o 3197	. 2 |- (F:A-1-1-onto->C <-> (F:A-1-1->C /\ F:A-onto->C))
5		df-f1o 3197	. 2 |- (F:B-1-1-onto->C <-> (F:B-1-1->C /\ F:B-onto->C))
6	3, 4, 5	3bitr4g 555	1 |- (A = B -> (F:A-1-1-onto->C <-> F:B-1-1-onto->C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956  -1-1->wf1 3179  -onto->wfo 3180  -1-1-onto->wf1o 3181

This theorem is referenced by:  isoeq4 3890  breng 4375  unfilem3 4550  icoshftf1olem 6410  infxpidmlem2 7553  infxpidmlem3 7554  infxpidmlem11 7562  shftefif1olem 8741  eff1o2 8754  elgiso 10398  symgval 10403  cayleylem3 10411  homeofval 10516

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469  df-fn 3193  df-f 3194  df-f1 3195  df-fo 3196  df-f1o 3197

Copyright terms: Public domain