Theorem f1oeq2 3680

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 3656	. . 3 |- (A = B -> (F:A-1-1->C <-> F:B-1-1->C))
2		foeq2 3664	. . 3 |- (A = B -> (F:A-onto->C <-> F:B-onto->C))
3	1, 2	anbi12d 627	. 2 |- (A = B -> ((F:A-1-1->C /\ F:A-onto->C) <-> (F:B-1-1->C /\ F:B-onto->C)))
4		df-f1o 3193	. 2 |- (F:A-1-1-onto->C <-> (F:A-1-1->C /\ F:A-onto->C))
5		df-f1o 3193	. 2 |- (F:B-1-1-onto->C <-> (F:B-1-1->C /\ F:B-onto->C))
6	3, 4, 5	3bitr4g 554	1 |- (A = B -> (F:A-1-1-onto->C <-> F:B-1-1-onto->C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 955  -1-1->wf1 3175  -onto->wfo 3176  -1-1-onto->wf1o 3177

This theorem is referenced by:  isoeq4 3885  breng 4366  unfilem3 4535  icoshftf1olem 6356  infxpidmlem2 7513  infxpidmlem3 7514  infxpidmlem11 7522  shftefif1olem 8696  eff1o2 8709  elgiso 10354  symgval 10359  cayleylem3 10367  homeofval 10462

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468  df-fn 3189  df-f 3190  df-f1 3191  df-fo 3192  df-f1o 3193

Copyright terms: Public domain