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

Theorem 2ralbii 3010
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 3009 . 2 (∀𝑦𝐵 𝜑 ↔ ∀𝑦𝐵 𝜓)
32ralbii 3009 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  cnvso  5712  fununi  6002  dff14a  6567  isocnv2  6621  sorpss  6984  tpossym  7429  dford2  8555  isffth2  16623  ispos2  16995  issubm  17394  cntzrec  17812  oppgsubm  17838  opprirred  18748  opprsubrg  18849  gsummatr01lem3  20511  gsummatr01  20513  isbasis2g  20800  ist0-3  21197  isfbas2  21686  isclmp  22943  dfadj2  28872  adjval2  28878  cnlnadjeui  29064  adjbdln  29070  rmo4f  29464  isarchi  29864  iccllysconn  31358  dfso3  31727  elpotr  31810  dfon2  31821  f1opr  33649  3ralbii  34155  idinxpss  34224  inxpssidinxp  34227  idinxpssinxp  34228  isltrn2N  35724  fphpd  37697  isdomn3  38099  fiinfi  38195  ntrk1k3eqk13  38665  ordelordALT  39064  2reu4a  41510  issubmgm  42114
  Copyright terms: Public domain W3C validator