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

Theorem r19.26-2 3047
Description: Restricted quantifier version of 19.26-2 1787. Version of r19.26 3046 with two quantifiers. (Contributed by NM, 10-Aug-2004.)
Assertion
Ref Expression
r19.26-2 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))

Proof of Theorem r19.26-2
StepHypRef Expression
1 r19.26 3046 . . 3 (∀𝑦𝐵 (𝜑𝜓) ↔ (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓))
21ralbii 2963 . 2 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓))
3 r19.26 3046 . 2 (∀𝑥𝐴 (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))
42, 3bitri 263 1 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  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-an 385  df-ral 2901
This theorem is referenced by:  fununi  5878  tz7.48lem  7423  isffth2  16399  ispos2  16771  issgrpv  17109  issgrpn0  17110  isnsg2  17447  efgred  17984  dfrhm2  18540  cpmatacl  20340  cpmatmcllem  20342  caucfil  22889  aalioulem6  23896  ajmoi  27098  adjmo  28075  iccllyscon  30486  dfso3  30856  ispridl2  33007  ishlat2  33658  fiinfi  36897  ntrk1k3eqk13  37368  isrnghm  41682
  Copyright terms: Public domain W3C validator