Theorem lebi 145

Description: "Less than or equal to" to biconditional. (Contributed by NM, 27-Aug-1997.)

Hypotheses

Ref	Expression
lebi.1	a ≤ b
lebi.2	b ≤ a

Assertion

Ref	Expression
lebi	a = b

Proof of Theorem lebi

Step	Hyp	Ref	Expression
1		lebi.2	. . . . 5 b ≤ a
2	1	df-le2 131	. . . 4 (b ∪ a) = a
3	2	ax-r1 35	. . 3 a = (b ∪ a)
4		ax-a2 31	. . 3 (b ∪ a) = (a ∪ b)
5	3, 4	ax-r2 36	. 2 a = (a ∪ b)
6		lebi.1	. . 3 a ≤ b
7	6	df-le2 131	. 2 (a ∪ b) = b
8	5, 7	ax-r2 36	1 a = b

Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36

This theorem depends on definitions:  df-le2 131

This theorem is referenced by:  distlem  188  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  wlem1  243  mccune2  247  wql1lem  287  wql2lem  288  womle2a  295  nom14  311  go1  343  k1-8a  355  2vwomlem  365  wr5-2v  366  wdf-c2  384  ska2  432  ska4  433  ka4ot  435  ortha  438  cmtr1com  493  i3or  497  i3ri3  538  i3li3  539  i32i3  540  ud4lem1a  577  i2bi  722  u12lem  771  u3lemax4  796  u3lemax5  797  bi1o1a  798  biao  799  i2i1i1  800  3vth2  805  3vded11  814  3vded12  815  1oaiii  823  3vroa  831  negant  852  negant3  860  negant4  862  neg3ant1  866  mhlem  876  mh  879  distid  887  oago3.21x  890  cancel  892  gomaex4  900  gomaex3lem2  915  oau  929  oa23  936  oaliii  1001  oagen1  1014  oadist  1019  oadistb  1020  oadistc0  1021  oadistc  1022  oadistd  1023  4oaiii  1040  4oagen1  1042  4oadist  1044  lem3.3.5lem  1054  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  com3iia  1102  lem4.6.7  1103  wdwom  1106  ml  1123  mldual2i  1127  ml3  1130  vneulem1  1131  vneulem6  1136  vneulem7  1137  vneulem13  1143  vneulemexp  1148