Theorem f1oeq3 3683

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

Assertion

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

Proof of Theorem f1oeq3

Step	Hyp	Ref	Expression
1		f1eq3 3659	. . 3 |- (A = B -> (F:C-1-1->A <-> F:C-1-1->B))
2		foeq3 3667	. . 3 |- (A = B -> (F:C-onto->A <-> F:C-onto->B))
3	1, 2	anbi12d 627	. 2 |- (A = B -> ((F:C-1-1->A /\ F:C-onto->A) <-> (F:C-1-1->B /\ F:C-onto->B)))
4		df-f1o 3194	. 2 |- (F:C-1-1-onto->A <-> (F:C-1-1->A /\ F:C-onto->A))
5		df-f1o 3194	. 2 |- (F:C-1-1-onto->B <-> (F:C-1-1->B /\ F:C-onto->B))
6	3, 4, 5	3bitr4g 554	1 |- (A = B -> (F:C-1-1-onto->A <-> F:C-1-1-onto->B))

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

This theorem is referenced by:  isoeq5 3888  ncanth 3905  breng 4370  idssen 4400  unfilem3 4539  icoshftf1olem 6361  reeff1o2 7405  nnenom 7476  unbenlem 7483  infxpidmlem2 7532  infxpidmlem3 7533  shftefif1olem 8725  adjbd1o 10009  elgiso 10389  symgval 10394  cayleylem3 10402  homeofval 10497

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2049  df-ss 2051  df-f 3191  df-f1 3192  df-fo 3193  df-f1o 3194

Copyright terms: Public domain