Theorem rexbidv2 2964

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
rexbidv2.1

Assertion

Ref	Expression
rexbidv2

Distinct variable group:   ,

Proof of Theorem rexbidv2

Step	Hyp	Ref	Expression
1		rexbidv2.1	. . 3
2	1	exbidv 1714	. 2
3		df-rex 2813	. 2
4		df-rex 2813	. 2
5	2, 3, 4	3bitr4g 288	1

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

This theorem is referenced by:  rexbidva  2965  rexss  3566  exopxfr2  5152  rexsuppOLD  6012  isoini  6234  rexsupp  6937  omabs  7315  elfi2  7894  wemapsolem  7996  ltexpi  9301  rexuz  11160  lpigen  17904  llyi  19975  nllyi  19976  elpi1  21545  xrecex  27616  mrefg2  30639  islssfg2  31017  fourierdlem71  31960  bnj18eq1  33985  ldual1dim  34891  pmapjat1  35577

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

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