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

Theorem 2ralbii 3169
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 3168 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 3168 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-ral 3101
This theorem is referenced by:  cnvso  5888  fununi  6171  dff14a  6747  isocnv2  6801  sorpss  7168  tpossym  7615  dford2  8760  isffth2  16776  ispos2  17149  issubm  17548  cntzrec  17963  oppgsubm  17989  opprirred  18900  opprsubrg  19001  gsummatr01lem3  20672  gsummatr01  20674  isbasis2g  20963  ist0-3  21360  isfbas2  21849  isclmp  23106  dfadj2  29071  adjval2  29077  cnlnadjeui  29263  adjbdln  29269  rmo4f  29662  isarchi  30060  iccllysconn  31553  dfso3  31921  elpotr  32004  dfon2  32015  f1opr  33829  3ralbii  34330  idinxpss  34397  inxpssidinxp  34400  idinxpssinxp  34401  isltrn2N  35898  fphpd  37879  isdomn3  38280  fiinfi  38375  ntrk1k3eqk13  38845  ordelordALT  39242  2reu4a  41698  issubmgm  42354
  Copyright terms: Public domain W3C validator