Theorem reubidva 3041

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)

Hypothesis

Ref	Expression
reubidva.1

Assertion

Ref	Expression
reubidva

Distinct variable group:   ,

Proof of Theorem reubidva

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		reubidva.1	. 2
3	1, 2	reubida 3040	1

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

This theorem is referenced by:  reubidv  3042  reuxfr2d  4675  reuxfrd  4677  exfo  6049  f1ofveu  6291  zmax  11208  zbtwnre  11209  rebtwnz  11210  icoshftf1o  11672  divalgb  14062  1arith2  14446  ply1divalg2  22539  frg2woteu  25055  numclwwlk2lem1  25102  numclwlk2lem2f1o  25105  addinv  25354  pjhtheu2  26334  reuxfr3d  27388  reuxfr4d  27389  xrsclat  27668  xrmulc1cn  27912  hdmap14lem14  37611

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