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

Theorem 2ralbii 3124
Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
Hypothesis
Ref Expression
2ralbii.1 (𝜑𝜓)
Assertion
Ref Expression
2ralbii (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)

Proof of Theorem 2ralbii
StepHypRef Expression
1 2ralbii.1 . . 3 (𝜑𝜓)
21ralbii 3093 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 3093 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  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
This theorem depends on definitions:  df-bi 206  df-ral 3062
This theorem is referenced by:  ralnex3  3128  rmo4f  3697  2reu4lem  4487  cnvso  6244  fununi  6580  dff14a  7221  isocnv2  7280  f1opr  7417  sorpss  7669  xpord3inddlem  8090  tpossym  8193  dford2  9564  isffth2  17811  ispos2  18212  issubm  18622  cntzrec  19122  oppgsubm  19151  opprirred  20141  opprsubrg  20285  gsummatr01lem3  22029  gsummatr01  22031  isbasis2g  22321  ist0-3  22719  isfbas2  23209  isclmp  24483  addsproplem4  27313  addsproplem6  27315  addsprop  27317  negsproplem4  27358  negsproplem6  27360  negsprop  27362  dfadj2  30876  adjval2  30882  cnlnadjeui  31068  adjbdln  31074  isarchi  32074  prmidl0  32278  dff15  33752  iccllysconn  33908  dfso3  34355  elpotr  34419  dfon2  34430  3ralbii  36758  idinxpss  36823  inxpssidinxp  36827  idinxpssinxp  36828  dfeldisj5  37233  isltrn2N  38633  isdomn5  40673  fphpd  41186  isdomn3  41578  fiinfi  41937  ntrk1k3eqk13  42414  ordelordALT  42911  disjinfi  43504  issubmgm  46173  isthinc2  47132  isthinc3  47133
  Copyright terms: Public domain W3C validator