Theorem rexex 2914

Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)

Assertion

Ref	Expression
rexex

Proof of Theorem rexex

Step	Hyp	Ref	Expression
1		df-rex 2813	. 2
2		exsimpr 1678	. 2
3	1, 2	sylbi 195	1

Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  reu3  3289  rmo2i  3428  dffo5  6048  nqerf  9329  supsrlem  9509  vdwmc2  14497  isch3  26159  19.9d2rf  27377  volfiniune  28202  dfrdg4  29600  mblfinlem3  30053  mblfinlem4  30054  stoweidlem57  31839  bnj594  33970  bnj1371  34085  bnj1374  34087  bj-0nelsngl  34529  bj-ccinftydisj  34616

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813