Theorem 2rexbidv 2975

Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1

Assertion

Ref	Expression
2rexbidv

Distinct variable groups:   ,   ,

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3
2	1	rexbidv 2968	. 2
3	2	rexbidv 2968	1

Syntax hints:  ->wi 4  <->wb 184  E.wrex 2808

This theorem is referenced by:  f1oiso  6247  elrnmpt2g  6414  elrnmpt2  6415  ralrnmpt2  6417  ovelrn  6451  opiota  6859  omeu  7253  oeeui  7270  eroveu  7425  erov  7427  elfiun  7910  dffi3  7911  xpwdomg  8032  brdom7disj  8930  brdom6disj  8931  genpv  9398  genpelv  9399  axcnre  9562  supmullem1  10534  supmullem2  10535  supmul  10536  sqrlem6  13081  ello1  13338  ello1mpt  13344  elo1  13349  lo1o1  13355  o1lo1  13360  bezoutlem1  14176  bezoutlem3  14178  bezoutlem4  14179  bezout  14180  pythagtriplem2  14341  pythagtriplem19  14357  pythagtrip  14358  pcval  14368  pceu  14370  pczpre  14371  pcdiv  14376  4sqlem2  14467  4sqlem3  14468  4sqlem4  14470  4sq  14482  vdwlem1  14499  vdwlem12  14510  vdwlem13  14511  vdwnnlem1  14513  vdwnnlem2  14514  vdwnnlem3  14515  vdwnn  14516  ramub2  14532  rami  14533  pgpfac1lem3  17128  lspprel  17740  znunit  18602  cayleyhamiltonALT  19392  hausnei  19829  isreg2  19878  txuni2  20066  txbas  20068  xkoopn  20090  txcls  20105  txcnpi  20109  txdis1cn  20136  txtube  20141  txcmplem1  20142  hausdiag  20146  tx1stc  20151  regr1lem2  20241  qustgplem  20619  met2ndci  21025  dyadmax  22007  i1fadd  22102  i1fmul  22103  elply  22592  2sqlem2  23639  2sqlem8  23647  2sqlem9  23648  2sqlem11  23650  istrkgld  23857  axtgeucl  23870  legov  23972  axsegconlem1  24220  axpasch  24244  axlowdim  24264  axeuclidlem  24265  nb3grapr  24453  el2wlksoton  24878  el2spthsoton  24879  el2wlksotot  24882  2wot2wont  24886  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  usg2spot2nb  25065  br8d  27463  pstmval  27874  eulerpartlemgh  28317  eulerpartlemgs2  28319  cvmliftlem15  28743  cvmlift2lem10  28757  br8  29185  br6  29186  br4  29187  nofulllem5  29466  elaltxp  29625  brsegle  29758  ellines  29802  supadd  30042  ptrest  30048  ismblfin  30055  itg2addnclem3  30068  itg2addnc  30069  nn0prpwlem  30140  nn0prpw  30141  mzpcompact2lem  30684  mzpcompact2  30685  sbc4rexgOLD  30723  pell1qrval  30782  elpell1qr  30783  pell14qrval  30784  elpell14qr  30785  pell1234qrval  30786  elpell1234qr  30787  jm2.27  30950  expdiophlem1  30963  limclner  31657  fourierdlem42  31931  fourierdlem48  31937  isline  35463  psubspi  35471  paddfval  35521  elpadd  35523  paddvaln0N  35525

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-an 371  df-ex 1613  df-rex 2813