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

Theorem 2ralbidv 3209
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 3171 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 3171 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3061
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 398  df-ral 3062
This theorem is referenced by:  3ralbidv  3212  cbvral3vw  3228  cbvral3v  3342  ralxpxfr2d  3597  poeq1  5549  soeq1  5567  isoeq1  7263  isoeq2  7264  isoeq3  7265  fnmpoovd  8020  xpord3inddlem  8087  smoeq  8297  xpf1o  9086  nqereu  10870  dedekind  11323  dedekindle  11324  seqcaopr2  13950  wrd2ind  14617  addcn2  15482  mulcn2  15484  mreexexd  17533  catlid  17568  catrid  17569  isfunc  17755  funcres2b  17788  isfull  17802  isfth  17806  fullres2c  17831  isnat  17839  evlfcl  18116  uncfcurf  18133  isprs  18191  isdrs  18195  ispos  18208  istos  18312  isdlat  18416  sgrp1  18560  ismhm  18608  issubm  18619  sgrp2nmndlem4  18743  isnsg  18962  isghm  19013  isga  19076  pmtrdifwrdel  19272  sylow2blem2  19408  efglem  19503  efgi  19506  efgredlemb  19533  efgred  19535  frgpuplem  19559  iscmn  19576  ring1  20031  isirred  20135  islmod  20340  lmodlema  20341  lssset  20409  islssd  20411  islmhm  20503  islmhm2  20514  isobs  21142  dmatel  21858  dmatmulcl  21865  scmateALT  21877  mdetunilem3  21979  mdetunilem4  21980  mdetunilem9  21985  cpmatel  22076  chpscmat  22207  hausnei2  22720  dfconn2  22786  llyeq  22837  nllyeq  22838  isucn2  23647  iducn  23651  ispsmet  23673  ismet  23692  isxmet  23693  metucn  23943  ngptgp  24008  nlmvscnlem1  24066  xmetdcn2  24216  addcnlem  24243  elcncf  24268  ipcnlem1  24625  cfili  24648  c1lip1  25377  aalioulem5  25712  aalioulem6  25713  aaliou  25714  aaliou2  25716  aaliou2b  25717  ulmcau  25770  ulmdvlem3  25777  cxpcn3lem  26116  dvdsmulf1o  26559  chpdifbndlem2  26918  pntrsumbnd2  26931  addsprop  27310  negsprop  27355  istrkgb  27439  axtgsegcon  27448  axtg5seg  27449  axtgpasch  27451  axtgeucl  27456  iscgrg  27496  isismt  27518  isperp2  27699  f1otrg  27855  axcontlem10  27964  axcontlem12  27966  iscusgredg  28413  isgrpo  29481  isablo  29530  vacn  29678  smcnlem  29681  lnoval  29736  islno  29737  isphg  29801  ajmoi  29842  ajval  29845  adjmo  30816  elcnop  30841  ellnop  30842  elunop  30856  elhmop  30857  elcnfn  30866  ellnfn  30867  adjeu  30873  adjval  30874  adj1  30917  adjeq  30919  cnlnadjlem9  31059  cnlnadjeu  31062  cnlnssadj  31064  isst  31197  ishst  31198  cdj1i  31417  cdj3i  31425  resspos  31875  resstos  31876  ismnt  31892  mgcval  31896  isomnd  31958  isslmd  32086  slmdlema  32087  isorng  32141  prmidlval  32257  isprmidl  32258  isrprm  32310  qqhucn  32630  ismntop  32664  axtgupdim2ALTV  33338  txpconn  33883  nn0prpw  34841  heicant  36159  equivbnd  36295  isismty  36306  heibor1lem  36314  iccbnd  36345  isass  36351  elghomlem1OLD  36390  elghomlem2OLD  36391  isrngohom  36470  iscom2  36500  pridlval  36538  ispridl  36539  isdmn3  36579  inecmo  36862  islfl  37568  isopos  37688  psubspset  38253  islaut  38592  ispautN  38608  ltrnset  38627  isltrn  38628  istrnN  38666  istendo  39269  sticksstones1  40600  sticksstones2  40601  sticksstones3  40602  sticksstones8  40607  sticksstones10  40609  sticksstones11  40610  sticksstones12a  40611  sticksstones15  40615  clsk1independent  42406  sprsymrelfolem2  45771  sprsymrelfo  45775  reuopreuprim  45804  ismgmhm  46163  issubmgm  46169  rnghmval  46275  isrnghm  46276  lidlmsgrp  46310  lidlrng  46311  dmatALTbasel  46569  lindslinindsimp2  46630  lmod1  46659  isnrm4  47049  iscnrm4  47073  isthinc  47127  thincciso  47155
  Copyright terms: Public domain W3C validator