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

Theorem 2ralbii 2963
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 2962 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 2962 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ral 2900
This theorem is referenced by:  cnvso  5576  fununi  5863  dff14a  6404  isocnv2  6458  sorpss  6817  tpossym  7248  dford2  8377  isffth2  16347  ispos2  16719  issubm  17118  cntzrec  17537  oppgsubm  17563  opprirred  18473  opprsubrg  18572  gsummatr01lem3  20229  gsummatr01  20231  isbasis2g  20510  ist0-3  20906  isfbas2  21396  isclmp  22652  dfadj2  27921  adjval2  27927  cnlnadjeui  28113  adjbdln  28119  rmo4f  28514  isarchi  28860  iccllyscon  30279  dfso3  30649  elpotr  30723  dfon2  30734  f1opr  32472  isltrn2N  34207  fphpd  36181  isdomn3  36584  fiinfi  36680  ntrk1k3eqk13  37151  ordelordALT  37551  2reu4a  39621  issubmgm  41560
  Copyright terms: Public domain W3C validator