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

Theorem 2ralbidv 3130
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
Hypothesis
Ref Expression
2ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2ralbidv (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2ralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21ralbidv 3113 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 3113 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3070
This theorem is referenced by:  cbvral3vw  3399  cbvral3v  3402  ralxpxfr2d  3577  poeq1  5507  soeq1  5525  isoeq1  7197  isoeq2  7198  isoeq3  7199  fnmpoovd  7936  smoeq  8190  xpf1o  8935  nqereu  10694  dedekind  11147  dedekindle  11148  seqcaopr2  13768  wrd2ind  14445  addcn2  15312  mulcn2  15314  mreexexd  17366  catlid  17401  catrid  17402  isfunc  17588  funcres2b  17621  isfull  17635  isfth  17639  fullres2c  17664  isnat  17672  evlfcl  17949  uncfcurf  17966  isprs  18024  isdrs  18028  ispos  18041  istos  18145  isdlat  18249  sgrp1  18393  ismhm  18441  issubm  18451  sgrp2nmndlem4  18576  isnsg  18792  isghm  18843  isga  18906  pmtrdifwrdel  19102  sylow2blem2  19235  efglem  19331  efgi  19334  efgredlemb  19361  efgred  19363  frgpuplem  19387  iscmn  19403  ring1  19850  isirred  19950  islmod  20136  lmodlema  20137  lssset  20204  islssd  20206  islmhm  20298  islmhm2  20309  isobs  20936  dmatel  21651  dmatmulcl  21658  scmateALT  21670  mdetunilem3  21772  mdetunilem4  21773  mdetunilem9  21778  cpmatel  21869  chpscmat  22000  hausnei2  22513  dfconn2  22579  llyeq  22630  nllyeq  22631  isucn2  23440  iducn  23444  ispsmet  23466  ismet  23485  isxmet  23486  metucn  23736  ngptgp  23801  nlmvscnlem1  23859  xmetdcn2  24009  addcnlem  24036  elcncf  24061  ipcnlem1  24418  cfili  24441  c1lip1  25170  aalioulem5  25505  aalioulem6  25506  aaliou  25507  aaliou2  25509  aaliou2b  25510  ulmcau  25563  ulmdvlem3  25570  cxpcn3lem  25909  dvdsmulf1o  26352  chpdifbndlem2  26711  pntrsumbnd2  26724  istrkgb  26825  axtgsegcon  26834  axtg5seg  26835  axtgpasch  26837  axtgeucl  26842  iscgrg  26882  isismt  26904  isperp2  27085  f1otrg  27241  axcontlem10  27350  axcontlem12  27352  iscusgredg  27799  isgrpo  28868  isablo  28917  vacn  29065  smcnlem  29068  lnoval  29123  islno  29124  isphg  29188  ajmoi  29229  ajval  29232  adjmo  30203  elcnop  30228  ellnop  30229  elunop  30243  elhmop  30244  elcnfn  30253  ellnfn  30254  adjeu  30260  adjval  30261  adj1  30304  adjeq  30306  cnlnadjlem9  30446  cnlnadjeu  30449  cnlnssadj  30451  isst  30584  ishst  30585  cdj1i  30804  cdj3i  30812  resspos  31253  resstos  31254  ismnt  31270  mgcval  31274  isomnd  31336  isslmd  31464  slmdlema  31465  isorng  31507  prmidlval  31621  isprmidl  31622  isrprm  31674  qqhucn  31951  ismntop  31985  axtgupdim2ALTV  32657  txpconn  33203  xpord3ind  33809  nn0prpw  34521  heicant  35821  equivbnd  35957  isismty  35968  heibor1lem  35976  iccbnd  36007  isass  36013  elghomlem1OLD  36052  elghomlem2OLD  36053  isrngohom  36132  iscom2  36162  pridlval  36200  ispridl  36201  isdmn3  36241  inecmo  36494  islfl  37081  isopos  37201  psubspset  37765  islaut  38104  ispautN  38120  ltrnset  38139  isltrn  38140  istrnN  38178  istendo  38781  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones15  40124  clsk1independent  41663  sprsymrelfolem2  44956  sprsymrelfo  44960  reuopreuprim  44989  ismgmhm  45348  issubmgm  45354  rnghmval  45460  isrnghm  45461  lidlmsgrp  45495  lidlrng  45496  dmatALTbasel  45754  lindslinindsimp2  45815  lmod1  45844  isnrm4  46235  iscnrm4  46259  isthinc  46313  thincciso  46341
  Copyright terms: Public domain W3C validator