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

Theorem 2rexbidv 2972
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 2965 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2965 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 184   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-rex 2810
This theorem is referenced by:  f1oiso  6222  elrnmpt2g  6387  elrnmpt2  6388  ralrnmpt2  6390  ovelrn  6424  opiota  6832  omeu  7226  oeeui  7243  eroveu  7398  erov  7400  elfiun  7882  dffi3  7883  xpwdomg  8003  brdom7disj  8900  brdom6disj  8901  genpv  9366  genpelv  9367  axcnre  9530  supmullem1  10504  supmullem2  10505  supmul  10506  sqrlem6  13163  ello1  13420  ello1mpt  13426  elo1  13431  lo1o1  13437  o1lo1  13442  bezoutlem1  14260  bezoutlem3  14262  bezoutlem4  14263  bezout  14264  pythagtriplem2  14425  pythagtriplem19  14441  pythagtrip  14442  pcval  14452  pceu  14454  pczpre  14455  pcdiv  14460  4sqlem2  14551  4sqlem3  14552  4sqlem4  14554  4sq  14566  vdwlem1  14583  vdwlem12  14594  vdwlem13  14595  vdwnnlem1  14597  vdwnnlem2  14598  vdwnnlem3  14599  vdwnn  14600  ramub2  14616  rami  14617  pgpfac1lem3  17323  lspprel  17935  znunit  18775  cayleyhamiltonALT  19559  hausnei  19996  isreg2  20045  txuni2  20232  txbas  20234  xkoopn  20256  txcls  20271  txcnpi  20275  txdis1cn  20302  txtube  20307  txcmplem1  20308  hausdiag  20312  tx1stc  20317  regr1lem2  20407  qustgplem  20785  met2ndci  21191  dyadmax  22173  i1fadd  22268  i1fmul  22269  elply  22758  2sqlem2  23837  2sqlem8  23845  2sqlem9  23846  2sqlem11  23848  istrkgld  24055  axtgeucl  24068  legov  24173  axsegconlem1  24422  axpasch  24446  axlowdim  24466  axeuclidlem  24467  nb3grapr  24655  el2wlksoton  25080  el2spthsoton  25081  el2wlksotot  25084  2wot2wont  25088  vdn0frgrav2  25225  vdgn0frgrav2  25226  vdn1frgrav2  25227  vdgn1frgrav2  25228  usg2spot2nb  25267  br8d  27678  pstmval  28109  eulerpartlemgh  28581  eulerpartlemgs2  28583  cvmliftlem15  29007  cvmlift2lem10  29021  br8  29426  br6  29427  br4  29428  nofulllem5  29706  elaltxp  29853  brsegle  29986  ellines  30030  supadd  30282  ptrest  30288  ismblfin  30295  itg2addnclem3  30308  itg2addnc  30309  nn0prpwlem  30380  nn0prpw  30381  mzpcompact2lem  30923  mzpcompact2  30924  sbc4rexgOLD  30963  pell1qrval  31021  elpell1qr  31022  pell14qrval  31023  elpell14qr  31024  pell1234qrval  31025  elpell1234qr  31026  jm2.27  31189  expdiophlem1  31202  limclner  31896  fourierdlem42  32170  fourierdlem48  32176  bigoval  33424  elbigo  33426  isline  35860  psubspi  35868  paddfval  35918  elpadd  35920  paddvaln0N  35922
  Copyright terms: Public domain W3C validator