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

Theorem 2ralbidv 2585
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
Hypothesis
Ref Expression
2ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2ralbidv  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. 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 2ralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2563 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32ralbidv 2563 1  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543
This theorem is referenced by:  cbvral3v  2774  poeq1  4317  soeq1  4333  isoeq1  5816  isoeq2  5817  isoeq3  5818  smoeq  6367  xpf1o  7023  nqereu  8553  seqcaopr2  11082  addcn2  12067  mulcn2  12069  mreexexd  13550  funcres2b  13771  isfull  13784  isfth  13788  fullres2c  13813  isnat  13821  evlfcl  13996  uncfcurf  14013  isprs  14064  isdrs  14068  ispos  14081  istos  14141  islat  14153  isdlat  14296  ismhm  14417  issubm  14425  isnsg  14646  isghm  14683  isga  14745  sylow2blem2  14932  efglem  15025  efgi  15028  efgredlemb  15055  efgred  15057  frgpuplem  15081  iscmn  15096  isirred  15481  islmod  15631  lmodlema  15632  lssset  15691  islssd  15693  islmhm  15784  islmhm2  15795  isobs  16620  hausnei2  17081  dfcon2  17145  llyeq  17196  nllyeq  17197  ismet  17888  isxmet  17889  ngptgp  18152  nlmvscnlem1  18197  xmetdcn2  18342  addcnlem  18368  elcncf  18393  ipcnlem1  18672  cfili  18694  c1lip1  19344  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou2  19720  aaliou2b  19721  ulmcau  19772  ulmdvlem3  19779  cxpcn3lem  20087  dvdsmulf1o  20434  chpdifbndlem2  20703  pntrsumbnd2  20716  isgrpo  20863  isablo  20950  isass  20983  elghomlem1  21028  elghomlem2  21029  iscom2  21079  vacn  21267  smcnlem  21270  lnoval  21330  islno  21331  isphg  21395  ajmoi  21437  ajval  21440  adjmo  22412  elcnop  22437  ellnop  22438  elunop  22452  elhmop  22453  elcnfn  22462  ellnfn  22463  adjeu  22469  adjval  22470  adj1  22513  adjeq  22515  cnlnadjlem9  22655  cnlnadjeu  22658  cnlnssadj  22660  isst  22793  ishst  22794  cdj1i  23013  cdj3i  23021  txpcon  23763  dedekind  24082  dedekindle  24083  nofulllem4  24359  nofulllem5  24360  axcontlem10  24601  axcontlem12  24603  islatalg  25183  isoriso  25212  isoriso2  25213  com2i  25416  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  ismona  25809  ismonb  25810  isepib  25820  isfunb  25835  issrc  25867  propsrc  25868  isnword  25986  isibg2  26110  isibcg  26191  nn0prpw  26239  equivbnd  26514  isismty  26525  heibor1lem  26533  iccbnd  26564  isrngohom  26596  pridlval  26658  ispridl  26659  isdmn3  26699  ralxpxfr2d  26760  isfrgra  28171  islfl  29250  isopos  29370  psubspset  29933  islaut  30272  ispautN  30288  ltrnset  30307  isltrn  30308  istrnN  30346  istendo  30949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator