Theorem reurex 3074

Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)

Assertion

Ref	Expression
reurex

Proof of Theorem reurex

Step	Hyp	Ref	Expression
1		reu5 3073	. 2
2	1	simplbi 460	1

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

This theorem is referenced by:  reu3  3289  sbcreu  3414  reusv7OLD  4664  reuxfrd  4677  weniso  6250  oawordex  7225  oaabs  7312  oaabs2  7313  supval2  7935  fisup2g  7947  nqerf  9329  qbtwnre  11427  modprm0  14330  meet0  15767  join0  15768  issrgid  17174  isringid  17224  lspsneu  17769  frgpcyg  18612  qtophmeo  20318  pjthlem2  21853  dyadmax  22007  quotlem  22696  frgra2v  24999  2pthfrgrarn  25009  frgrancvvdeqlemC  25039  frg2wotn0  25056  pjhthlem2  26310  cnlnadj  26998  reuxfr4d  27389  rmoxfrdOLD  27391  rmoxfrd  27392  cvmliftpht  28763  tz6.26  29285  2reu2rex  32188  2rexreu  32190  2reu4  32195  isringrng  32687  uzlidlring  32735  lcfl7N  37228

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