Theorem reu5 3073

Description: Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)

Assertion

Ref	Expression
reu5

Proof of Theorem reu5

Step	Hyp	Ref	Expression
1		eu5 2310	. 2
2		df-reu 2814	. 2
3		df-rex 2813	. . 3
4		df-rmo 2815	. . 3
5	3, 4	anbi12i 697	. 2
6	1, 2, 5	3bitr4i 277	1

Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E!weu 2282  E*wmo 2283  E.wrex 2808  E!wreu 2809  E*wrmo 2810

This theorem is referenced by:  reurex  3074  reurmo  3075  reu4  3293  reueq  3297  reusv1  4652  wereu  4880  wereu2  4881  fncnv  5657  moriotass  6286  supeu  7934  resqreu  13086  sqrtneg  13101  sqreu  13193  catideu  15072  poslubd  15778  ismgmid  15891  mndideu  15934  evlseu  18185  frlmup4  18835  ply1divalg  22538  tglinethrueu  24019  foot  24096  mideu  24112  pjhtheu  26312  pjpreeq  26316  cnlnadjeui  26996  cvmliftlem14  28742  cvmlift2lem13  28760  cvmlift3  28773  linethrueu  29806  2reu5a  32182  reuan  32185  2reurex  32186  2rexreu  32190  2reu1  32191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-eu 2286  df-mo 2287  df-rex 2813  df-reu 2814  df-rmo 2815