Theorem reurmo 3075

Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)

Assertion

Ref	Expression
reurmo

Proof of Theorem reurmo

Step	Hyp	Ref	Expression
1		reu5 3073	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  E.wrex 2808  E!wreu 2809  E*wrmo 2810

This theorem is referenced by:  reuxfrd  4677  enqeq  9333  eqsqrtd  13200  efgred2  16771  0frgp  16797  frgpnabllem2  16878  frgpcyg  18612  lmieu  24150  reuxfr4d  27389  reuimrmo  32183  2reurmo  32187  2rexreu  32190  2reu2  32192

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