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

Theorem 2ralbii 2964
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 2963 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 2963 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  cnvso  5591  fununi  5878  dff14a  6427  isocnv2  6481  sorpss  6840  tpossym  7271  dford2  8400  isffth2  16399  ispos2  16771  issubm  17170  cntzrec  17589  oppgsubm  17615  opprirred  18525  opprsubrg  18624  gsummatr01lem3  20282  gsummatr01  20284  isbasis2g  20563  ist0-3  20959  isfbas2  21449  isclmp  22705  dfadj2  28128  adjval2  28134  cnlnadjeui  28320  adjbdln  28326  rmo4f  28721  isarchi  29067  iccllyscon  30486  dfso3  30856  elpotr  30930  dfon2  30941  f1opr  32689  isltrn2N  34424  fphpd  36398  isdomn3  36801  fiinfi  36897  ntrk1k3eqk13  37368  ordelordALT  37768  2reu4a  39838  issubmgm  41579
  Copyright terms: Public domain W3C validator