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

Theorem 2ralbidv 2598
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 2576 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32ralbidv 2576 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 2556
This theorem is referenced by:  cbvral3v  2787  poeq1  4333  soeq1  4349  isoeq1  5832  isoeq2  5833  isoeq3  5834  smoeq  6383  xpf1o  7039  nqereu  8569  seqcaopr2  11098  addcn2  12083  mulcn2  12085  mreexexd  13566  funcres2b  13787  isfull  13800  isfth  13804  fullres2c  13829  isnat  13837  evlfcl  14012  uncfcurf  14029  isprs  14080  isdrs  14084  ispos  14097  istos  14157  islat  14169  isdlat  14312  ismhm  14433  issubm  14441  isnsg  14662  isghm  14699  isga  14761  sylow2blem2  14948  efglem  15041  efgi  15044  efgredlemb  15071  efgred  15073  frgpuplem  15097  iscmn  15112  isirred  15497  islmod  15647  lmodlema  15648  lssset  15707  islssd  15709  islmhm  15800  islmhm2  15811  isobs  16636  hausnei2  17097  dfcon2  17161  llyeq  17212  nllyeq  17213  ismet  17904  isxmet  17905  ngptgp  18168  nlmvscnlem1  18213  xmetdcn2  18358  addcnlem  18384  elcncf  18409  ipcnlem1  18688  cfili  18710  c1lip1  19360  aalioulem5  19732  aalioulem6  19733  aaliou  19734  aaliou2  19736  aaliou2b  19737  ulmcau  19788  ulmdvlem3  19795  cxpcn3lem  20103  dvdsmulf1o  20450  chpdifbndlem2  20719  pntrsumbnd2  20732  isgrpo  20879  isablo  20966  isass  20999  elghomlem1  21044  elghomlem2  21045  iscom2  21095  vacn  21283  smcnlem  21286  lnoval  21346  islno  21347  isphg  21411  ajmoi  21453  ajval  21456  adjmo  22428  elcnop  22453  ellnop  22454  elunop  22468  elhmop  22469  elcnfn  22478  ellnfn  22479  adjeu  22485  adjval  22486  adj1  22529  adjeq  22531  cnlnadjlem9  22671  cnlnadjeu  22674  cnlnssadj  22676  isst  22809  ishst  22810  cdj1i  23029  cdj3i  23037  txpcon  23778  dedekind  24097  dedekindle  24098  nofulllem4  24430  nofulllem5  24431  axcontlem10  24673  axcontlem12  24675  islatalg  25286  isoriso  25315  isoriso2  25316  com2i  25519  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  ismona  25912  ismonb  25913  isepib  25923  isfunb  25938  issrc  25970  propsrc  25971  isnword  26089  isibg2  26213  isibcg  26294  nn0prpw  26342  equivbnd  26617  isismty  26628  heibor1lem  26636  iccbnd  26667  isrngohom  26699  pridlval  26761  ispridl  26762  isdmn3  26802  ralxpxfr2d  26863  isfrgra  28417  islfl  29872  isopos  29992  psubspset  30555  islaut  30894  ispautN  30910  ltrnset  30929  isltrn  30930  istrnN  30968  istendo  31571
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator