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

Theorem 2rexbidv 2750
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 2728 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2728 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E.wrex 2708
This theorem is referenced by:  f1oiso  6074  elrnmpt2g  6185  elrnmpt2  6186  ralrnmpt2  6187  ovelrn  6225  opiota  6538  omeu  6831  oeeui  6848  eroveu  7002  erov  7004  elfiun  7438  dffi3  7439  xpwdomg  7556  brdom7disj  8414  brdom6disj  8415  genpv  8881  genpelv  8882  axcnre  9044  supmullem1  9979  supmullem2  9980  supmul  9981  sqrlem6  12058  ello1  12314  ello1mpt  12320  elo1  12325  lo1o1  12331  o1lo1  12336  bezoutlem1  13043  bezoutlem3  13045  bezoutlem4  13046  bezout  13047  pythagtriplem2  13196  pythagtriplem19  13212  pythagtrip  13213  pcval  13223  pceu  13225  pczpre  13226  pcdiv  13231  4sqlem2  13322  4sqlem3  13323  4sqlem4  13325  4sq  13337  vdwlem1  13354  vdwlem12  13365  vdwlem13  13366  vdwnnlem1  13368  vdwnnlem2  13369  vdwnnlem3  13370  vdwnn  13371  ramub2  13387  rami  13388  pgpfac1lem3  15640  lspprel  16171  znunit  16849  hausnei  17397  isreg2  17446  txuni2  17602  txbas  17604  xkoopn  17626  txcls  17641  txcnpi  17645  txdis1cn  17672  txtube  17677  txcmplem1  17678  hausdiag  17682  tx1stc  17687  regr1lem2  17777  divstgplem  18155  met2ndci  18557  dyadmax  19495  i1fadd  19590  i1fmul  19591  elply  20119  2sqlem2  21153  2sqlem8  21161  2sqlem9  21162  2sqlem11  21164  nb3grapr  21467  pstmval  24295  cvmliftlem15  24990  cvmlift2lem10  25004  br8  25384  br6  25385  br4  25386  nofulllem5  25666  elaltxp  25825  axsegconlem1  25861  axpasch  25885  axlowdim  25905  axeuclidlem  25906  brsegle  26047  ellines  26091  supadd  26246  ismblfin  26258  itg2addnclem3  26271  itg2addnc  26272  nn0prpwlem  26338  nn0prpw  26339  mzpcompact2lem  26821  mzpcompact2  26822  sbc4rexg  26858  pell1qrval  26922  elpell1qr  26923  pell14qrval  26924  elpell14qr  26925  pell1234qrval  26926  elpell1234qr  26927  jm2.27  27092  expdiophlem1  27105  el2wlksoton  28409  el2spthsoton  28410  el2wlksotot  28413  vdn0frgrav2  28487  vdgn0frgrav2  28488  vdn1frgrav2  28489  vdgn1frgrav2  28490  usg2spot2nb  28527  isline  30609  psubspi  30617  paddfval  30667  elpadd  30669  paddvaln0N  30671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-rex 2713
  Copyright terms: Public domain W3C validator