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

Theorem 2ralbidv 2747
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 2725 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32ralbidv 2725 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 177   A.wral 2705
This theorem is referenced by:  cbvral3v  2942  poeq1  4506  soeq1  4522  isoeq1  6039  isoeq2  6040  isoeq3  6041  smoeq  6612  xpf1o  7269  nqereu  8806  seqcaopr2  11359  addcn2  12387  mulcn2  12389  mreexexd  13873  catlid  13908  catrid  13909  isfunc  14061  funcres2b  14094  isfull  14107  isfth  14111  fullres2c  14136  isnat  14144  evlfcl  14319  uncfcurf  14336  isprs  14387  isdrs  14391  ispos  14404  istos  14464  islat  14476  isdlat  14619  ismhm  14740  issubm  14748  isnsg  14969  isghm  15006  isga  15068  sylow2blem2  15255  efglem  15348  efgi  15351  efgredlemb  15378  efgred  15380  frgpuplem  15404  iscmn  15419  isirred  15804  islmod  15954  lmodlema  15955  lssset  16010  islssd  16012  islmhm  16103  islmhm2  16114  isobs  16947  hausnei2  17417  dfcon2  17482  llyeq  17533  nllyeq  17534  isucn2  18309  iducn  18313  ispsmet  18335  ismet  18353  isxmet  18354  metucnOLD  18618  metucn  18619  ngptgp  18677  nlmvscnlem1  18722  xmetdcn2  18868  addcnlem  18894  elcncf  18919  ipcnlem1  19199  cfili  19221  c1lip1  19881  aalioulem5  20253  aalioulem6  20254  aaliou  20255  aaliou2  20257  aaliou2b  20258  ulmcau  20311  ulmdvlem3  20318  cxpcn3lem  20631  dvdsmulf1o  20979  chpdifbndlem2  21248  pntrsumbnd2  21261  isgrpo  21784  isablo  21871  isass  21904  elghomlem1  21949  elghomlem2  21950  iscom2  22000  vacn  22190  smcnlem  22193  lnoval  22253  islno  22254  isphg  22318  ajmoi  22360  ajval  22363  adjmo  23335  elcnop  23360  ellnop  23361  elunop  23375  elhmop  23376  elcnfn  23385  ellnfn  23386  adjeu  23392  adjval  23393  adj1  23436  adjeq  23438  cnlnadjlem9  23578  cnlnadjeu  23581  cnlnssadj  23583  isst  23716  ishst  23717  cdj1i  23936  cdj3i  23944  resspos  24187  resstos  24188  isofld  24235  qqhucn  24376  txpcon  24919  dedekind  25187  dedekindle  25188  nofulllem4  25660  nofulllem5  25661  axcontlem10  25912  axcontlem12  25914  nn0prpw  26326  equivbnd  26499  isismty  26510  heibor1lem  26518  iccbnd  26549  isrngohom  26581  pridlval  26643  ispridl  26644  isdmn3  26684  ralxpxfr2d  26741  isfrgra  28380  islfl  29858  isopos  29978  psubspset  30541  islaut  30880  ispautN  30896  ltrnset  30915  isltrn  30916  istrnN  30954  istendo  31557
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 2710
  Copyright terms: Public domain W3C validator