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

Theorem rexralbidv 2741
Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.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 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2717 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2718 1  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2697   E.wrex 2698
This theorem is referenced by:  freq1  4544  rexfiuz  12143  cau3lem  12150  caubnd2  12153  climi  12296  rlimi  12299  o1lo1  12323  2clim  12358  lo1le  12437  caucvgrlem  12458  caurcvgr  12459  caucvgb  12465  vdwlem10  13350  vdwlem13  13353  neiptopnei  17188  lmcvg  17318  lmss  17354  elpt  17596  elptr  17597  txlm  17672  tsmsi  18155  ustuqtop4  18266  isucn  18300  isucn2  18301  ucnima  18303  metcnpi  18566  metcnpi2  18567  metucnOLD  18610  metucn  18611  xrge0tsms  18857  elcncf  18911  cncfi  18916  lmmcvg  19206  lhop1  19890  ulmval  20288  ulmi  20294  ulmcaulem  20302  ulmdvlem3  20310  pntibnd  21279  pntlem3  21295  pntleml  21297  isgrpo  21776  ubthlem3  22366  ubth  22367  hcau  22678  hcaucvg  22680  hlimi  22682  hlimconvi  22685  hlim2  22686  elcnop  23352  elcnfn  23377  cnopc  23408  cnfnc  23425  lnopcon  23530  lnfncon  23551  riesz1  23560  xrge0tsmsd  24215  brbtwn  25830
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator