MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rexbidv Structured version   Unicode version

Theorem 2rexbidv 2880
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2rexbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2rexbidv  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x, y)    B( x, y)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2rexbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21rexbidv 2873 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2873 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E.wrex 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-rex 2715
This theorem is referenced by:  f1oiso  6196  elrnmpt2g  6361  elrnmpt2  6362  ralrnmpt2  6364  ovelrn  6398  opiota  6805  omeu  7236  oeeui  7253  eroveu  7408  erov  7410  elfiun  7892  dffi3  7893  xpwdomg  8048  brdom7disj  8905  brdom6disj  8906  genpv  9370  genpelv  9371  axcnre  9534  supadd  10521  supmullem1  10523  supmullem2  10524  supmul  10525  sqrlem6  13250  ello1  13517  ello1mpt  13523  elo1  13528  lo1o1  13534  o1lo1  13539  bezoutlem1  14441  bezoutlem3OLD  14443  bezoutlem4OLD  14444  bezoutlem3  14446  bezoutlem4  14447  bezout  14448  pythagtriplem2  14705  pythagtriplem19  14721  pythagtrip  14722  pcval  14732  pceu  14734  pczpre  14735  pcdiv  14740  4sqlem2  14831  4sqlem3  14832  4sqlem4  14834  4sq  14852  vdwlem1  14869  vdwlem12  14880  vdwlem13  14881  vdwnnlem1  14883  vdwnnlem2  14884  vdwnnlem3  14885  vdwnn  14886  ramub2  14909  rami  14910  pgpfac1lem3  17648  lspprel  18255  znunit  19071  cayleyhamiltonALT  19852  hausnei  20281  isreg2  20330  txuni2  20517  txbas  20519  xkoopn  20541  txcls  20556  txcnpi  20560  txdis1cn  20587  txtube  20592  txcmplem1  20593  hausdiag  20597  tx1stc  20602  regr1lem2  20692  qustgplem  21072  met2ndci  21474  dyadmax  22493  i1fadd  22590  i1fmul  22591  elply  23086  2sqlem2  24229  2sqlem8  24237  2sqlem9  24238  2sqlem11  24240  istrkgld  24444  axtgeucl  24457  legov  24567  iscgra  24788  dfcgra2  24808  axsegconlem1  24884  axpasch  24908  axlowdim  24928  axeuclidlem  24929  nb3grapr  25118  el2wlksoton  25543  el2spthsoton  25544  el2wlksotot  25547  2wot2wont  25551  vdn0frgrav2  25688  vdgn0frgrav2  25689  vdn1frgrav2  25690  vdgn1frgrav2  25691  usg2spot2nb  25730  br8d  28159  pstmval  28645  eulerpartlemgh  29158  eulerpartlemgs2  29160  cvmliftlem15  29968  cvmlift2lem10  29982  br8  30342  br6  30343  br4  30344  nofulllem5  30539  elaltxp  30686  brsegle  30819  ellines  30863  nn0prpwlem  30922  nn0prpw  30923  ptrest  31846  ismblfin  31888  itg2addnclem3  31902  itg2addnc  31903  isline  33216  psubspi  33224  paddfval  33274  elpadd  33276  paddvaln0N  33278  mzpcompact2lem  35505  mzpcompact2  35506  sbc4rexgOLD  35545  pell1qrval  35605  elpell1qr  35606  pell14qrval  35607  elpell14qr  35608  pell1234qrval  35609  elpell1234qr  35610  jm2.27  35776  expdiophlem1  35789  limclner  37615  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  isgbe  38665  isgbo  38666  isgboa  38667  sgoldbalt  38695  nnsum3primesle9  38702  nb3grpr  39187  bigoval  39953  elbigo  39955
  Copyright terms: Public domain W3C validator