Theorem lebi 137

Description: L.e. to biconditional.

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 123	. . . 4 (b ∪ a) = a
3	2	ax-r1 34	. . 3 a = (b ∪ a)
4		ax-a2 30	. . 3 (b ∪ a) = (a ∪ b)
5	3, 4	ax-r2 35	. 2 a = (a ∪ b)
6		lebi.1	. . 3 a ≤ b
7	6	df-le2 123	. 2 (a ∪ b) = b
8	5, 7	ax-r2 35	1 a = b

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

This theorem is referenced by:  distlem 180  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  ka4lemo 220  wlem1 235  mccune2 239  wql1lem 279  wql2lem 280  womle2a 287  nom14 303  go1 335  2vwomlem 347  wr5-2v 348  wdf-c2 366  ska2 414  ska4 415  ka4ot 417  ortha 420  cmtr1com 475  i3or 479  i3ri3 520  i3li3 521  i32i3 522  ud4lem1a 559  i2bi 704  u12lem 753  u3lemax4 778  u3lemax5 779  bi1o1a 780  biao 781  i2i1i1 782  3vth2 787  3vded11 796  3vded12 797  1oaiii 805  3vroa 813  negant 834  negant3 842  negant4 844  neg3ant1 848  mhlem 858  mh 861  distid 869  oago3.21x 872  cancel 874  gomaex4 880  gomaex3lem2 895  oau 909  oa23 916  oaliii 981  oagen1 994  oadist 999  oadistb 1000  oadistc0 1001  oadistc 1002  oadistd 1003  4oaiii 1019  4oagen1 1021  4oadist 1023

This theorem was proved from axioms:  ax-a2 30  ax-r1 34  ax-r2 35

This theorem depends on definitions:  df-le2 123

metamath.org