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

Theorem 2rexbidv 2753
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.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 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21rexbidv 2731 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2731 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 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-rex 2716
This theorem is referenced by:  f1oiso  6037  elrnmpt2g  6197  elrnmpt2  6198  ralrnmpt2  6200  ovelrn  6234  opiota  6628  omeu  7016  oeeui  7033  eroveu  7187  erov  7189  elfiun  7672  dffi3  7673  xpwdomg  7792  brdom7disj  8690  brdom6disj  8691  genpv  9160  genpelv  9161  axcnre  9323  supmullem1  10288  supmullem2  10289  supmul  10290  sqrlem6  12729  ello1  12985  ello1mpt  12991  elo1  12996  lo1o1  13002  o1lo1  13007  bezoutlem1  13714  bezoutlem3  13716  bezoutlem4  13717  bezout  13718  pythagtriplem2  13876  pythagtriplem19  13892  pythagtrip  13893  pcval  13903  pceu  13905  pczpre  13906  pcdiv  13911  4sqlem2  14002  4sqlem3  14003  4sqlem4  14005  4sq  14017  vdwlem1  14034  vdwlem12  14045  vdwlem13  14046  vdwnnlem1  14048  vdwnnlem2  14049  vdwnnlem3  14050  vdwnn  14051  ramub2  14067  rami  14068  pgpfac1lem3  16568  lspprel  17155  znunit  17976  hausnei  18912  isreg2  18961  txuni2  19118  txbas  19120  xkoopn  19142  txcls  19157  txcnpi  19161  txdis1cn  19188  txtube  19193  txcmplem1  19194  hausdiag  19198  tx1stc  19203  regr1lem2  19293  divstgplem  19671  met2ndci  20077  dyadmax  21058  i1fadd  21153  i1fmul  21154  elply  21643  2sqlem2  22683  2sqlem8  22691  2sqlem9  22692  2sqlem11  22694  axtgeucl  22913  legov  22996  axsegconlem1  23131  axpasch  23155  axlowdim  23175  axeuclidlem  23176  nb3grapr  23329  br8d  25910  pstmval  26291  eulerpartlemgh  26730  eulerpartlemgs2  26732  cvmliftlem15  27156  cvmlift2lem10  27170  br8  27535  br6  27536  br4  27537  nofulllem5  27816  elaltxp  27975  brsegle  28108  ellines  28152  supadd  28389  ptrest  28396  ismblfin  28403  itg2addnclem3  28416  itg2addnc  28417  nn0prpwlem  28488  nn0prpw  28489  mzpcompact2lem  29059  mzpcompact2  29060  sbc4rexgOLD  29099  pell1qrval  29158  elpell1qr  29159  pell14qrval  29160  elpell14qr  29161  pell1234qrval  29162  elpell1234qr  29163  jm2.27  29328  expdiophlem1  29341  el2wlksoton  30368  el2spthsoton  30369  el2wlksotot  30372  vdn0frgrav2  30587  vdgn0frgrav2  30588  vdn1frgrav2  30589  vdgn1frgrav2  30590  usg2spot2nb  30629  isline  33276  psubspi  33284  paddfval  33334  elpadd  33336  paddvaln0N  33338
  Copyright terms: Public domain W3C validator