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

Theorem rexralbidv 2962
Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2rexbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rexralbidv  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. 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 rexralbidv
StepHypRef Expression
1 2rexbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2882 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2954 1  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2793   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  freq1  4839  rexfiuz  13159  cau3lem  13166  caubnd2  13169  climi  13312  rlimi  13315  o1lo1  13339  2clim  13374  lo1le  13453  caucvgrlem  13474  caurcvgr  13475  caucvgb  13481  vdwlem10  14385  vdwlem13  14388  pmatcollpw2lem  19151  neiptopnei  19506  lmcvg  19636  lmss  19672  elpt  19946  elptr  19947  txlm  20022  tsmsi  20505  ustuqtop4  20620  isucn  20654  isucn2  20655  ucnima  20657  metcnpi  20920  metcnpi2  20921  metucnOLD  20964  metucn  20965  xrge0tsms  21212  elcncf  21266  cncfi  21271  lmmcvg  21573  lhop1  22288  ulmval  22647  ulmi  22653  ulmcaulem  22661  ulmdvlem3  22669  pntibnd  23650  pntlem3  23666  pntleml  23668  axtgcont1  23737  perpln1  23959  perpln2  23960  isperp  23961  brbtwn  24074  isgrpo  25070  ubthlem3  25660  ubth  25661  hcau  25973  hcaucvg  25975  hlimi  25977  hlimconvi  25980  hlim2  25981  elcnop  26648  elcnfn  26673  cnopc  26704  cnfnc  26721  lnopcon  26826  lnfncon  26847  riesz1  26856  xrge0tsmsd  27648  signsply0  28381  limcleqr  31558  addlimc  31562  0ellimcdiv  31563  cncfshift  31583  cncfperiod  31588  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  fourierdlem68  31846  fourierdlem87  31865  fourierdlem103  31881  fourierdlem104  31882
  Copyright terms: Public domain W3C validator