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

Theorem 2ralbii 3119
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 3118 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 3118 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ral 3055
This theorem is referenced by:  cnvso  5835  fununi  6125  dff14a  6691  isocnv2  6745  sorpss  7108  tpossym  7554  dford2  8692  isffth2  16797  ispos2  17169  issubm  17568  cntzrec  17986  oppgsubm  18012  opprirred  18922  opprsubrg  19023  gsummatr01lem3  20685  gsummatr01  20687  isbasis2g  20974  ist0-3  21371  isfbas2  21860  isclmp  23117  dfadj2  29074  adjval2  29080  cnlnadjeui  29266  adjbdln  29272  rmo4f  29666  isarchi  30066  iccllysconn  31560  dfso3  31929  elpotr  32012  dfon2  32023  f1opr  33850  3ralbii  34356  idinxpss  34425  inxpssidinxp  34428  idinxpssinxp  34429  isltrn2N  35927  fphpd  37900  isdomn3  38302  fiinfi  38398  ntrk1k3eqk13  38868  ordelordALT  39267  2reu4a  41713  issubmgm  42317
  Copyright terms: Public domain W3C validator