Theorem reubidv 3042

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.)

Hypothesis

Ref	Expression
reubidv.1

Assertion

Ref	Expression
reubidv

Distinct variable group:   ,

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		reubidv.1	. . 3
2	1	adantr 465	. 2
3	2	reubidva 3041	1

Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  E!wreu 2809

This theorem is referenced by:  reueqd  3064  sbcreu  3414  sbcreugOLD  3415  reusv6OLD  4663  reusv7OLD  4664  oawordeu  7223  xpf1o  7699  dfac2  8532  creur  10555  creui  10556  divalg  14061  divalg2  14063  lubfval  15608  lubeldm  15611  lubval  15614  glbfval  15621  glbeldm  15624  glbval  15627  joineu  15640  meeteu  15654  dfod2  16586  ustuqtop  20749  isfrgra  24990  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  3vfriswmgra  25005  n4cyclfrgra  25018  riesz4  26983  cnlnadjeu  26997  hdmap1eulem  37551  hdmap1eulemOLDN  37552  hdmap14lem6  37603

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  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-reu 2814