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

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

Proof of Theorem 2ralbii
StepHypRef Expression
1 ralbii.1 . . 3 (𝜑𝜓)
21ralbii 3133 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 3133 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ral 3111 This theorem is referenced by:  ralnex3  3222  rmo4f  3674  2reu4lem  4423  cnvso  6107  fununi  6399  dff14a  7006  isocnv2  7063  f1opr  7189  sorpss  7434  tpossym  7907  dford2  9067  isffth2  17178  ispos2  17550  issubm  17960  cntzrec  18456  oppgsubm  18482  opprirred  19448  opprsubrg  19549  gsummatr01lem3  21262  gsummatr01  21264  isbasis2g  21553  ist0-3  21950  isfbas2  22440  isclmp  23702  dfadj2  29668  adjval2  29674  cnlnadjeui  29860  adjbdln  29866  isarchi  30861  prmidl0  31034  dff15  32463  iccllysconn  32610  dfso3  33063  elpotr  33139  dfon2  33150  3ralbii  35670  idinxpss  35730  inxpssidinxp  35733  idinxpssinxp  35734  dfeldisj5  36114  isltrn2N  37416  fphpd  39755  isdomn3  40146  fiinfi  40270  ntrk1k3eqk13  40751  ordelordALT  41241  disjinfi  41818  issubmgm  44407
 Copyright terms: Public domain W3C validator