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

Theorem 2rexbidv 2862
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 2844 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2844 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 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-rex 2801
This theorem is referenced by:  f1oiso  6141  elrnmpt2g  6302  elrnmpt2  6303  ralrnmpt2  6305  ovelrn  6339  opiota  6733  omeu  7124  oeeui  7141  eroveu  7295  erov  7297  elfiun  7781  dffi3  7782  xpwdomg  7901  brdom7disj  8799  brdom6disj  8800  genpv  9269  genpelv  9270  axcnre  9432  supmullem1  10397  supmullem2  10398  supmul  10399  sqrlem6  12839  ello1  13095  ello1mpt  13101  elo1  13106  lo1o1  13112  o1lo1  13117  bezoutlem1  13824  bezoutlem3  13826  bezoutlem4  13827  bezout  13828  pythagtriplem2  13986  pythagtriplem19  14002  pythagtrip  14003  pcval  14013  pceu  14015  pczpre  14016  pcdiv  14021  4sqlem2  14112  4sqlem3  14113  4sqlem4  14115  4sq  14127  vdwlem1  14144  vdwlem12  14155  vdwlem13  14156  vdwnnlem1  14158  vdwnnlem2  14159  vdwnnlem3  14160  vdwnn  14161  ramub2  14177  rami  14178  pgpfac1lem3  16683  lspprel  17281  znunit  18105  hausnei  19048  isreg2  19097  txuni2  19254  txbas  19256  xkoopn  19278  txcls  19293  txcnpi  19297  txdis1cn  19324  txtube  19329  txcmplem1  19330  hausdiag  19334  tx1stc  19339  regr1lem2  19429  divstgplem  19807  met2ndci  20213  dyadmax  21194  i1fadd  21289  i1fmul  21290  elply  21779  2sqlem2  22819  2sqlem8  22827  2sqlem9  22828  2sqlem11  22830  axtgeucl  23050  legov  23137  axsegconlem1  23298  axpasch  23322  axlowdim  23342  axeuclidlem  23343  nb3grapr  23496  br8d  26076  pstmval  26456  eulerpartlemgh  26895  eulerpartlemgs2  26897  cvmliftlem15  27321  cvmlift2lem10  27335  br8  27700  br6  27701  br4  27702  nofulllem5  27981  elaltxp  28140  brsegle  28273  ellines  28317  supadd  28556  ptrest  28563  ismblfin  28570  itg2addnclem3  28583  itg2addnc  28584  nn0prpwlem  28655  nn0prpw  28656  mzpcompact2lem  29226  mzpcompact2  29227  sbc4rexgOLD  29266  pell1qrval  29325  elpell1qr  29326  pell14qrval  29327  elpell14qr  29328  pell1234qrval  29329  elpell1234qr  29330  jm2.27  29495  expdiophlem1  29508  el2wlksoton  30535  el2spthsoton  30536  el2wlksotot  30539  vdn0frgrav2  30754  vdgn0frgrav2  30755  vdn1frgrav2  30756  vdgn1frgrav2  30757  usg2spot2nb  30796  isline  33689  psubspi  33697  paddfval  33747  elpadd  33749  paddvaln0N  33751
  Copyright terms: Public domain W3C validator