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 3138
Description: Restricted quantifier version of 19.26-2 1874. Version of r19.26 3111 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 3111 . . 3 (∀𝑦𝐵 (𝜑𝜓) ↔ (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓))
21ralbii 3093 . 2 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∀𝑥𝐴 (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓))
3 r19.26 3111 . 2 (∀𝑥𝐴 (∀𝑦𝐵 𝜑 ∧ ∀𝑦𝐵 𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))
42, 3bitri 274 1 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062
This theorem is referenced by:  fununi  6623  tz7.48lem  8440  isffth2  17866  ispos2  18267  issgrpv  18611  issgrpn0  18612  isnsg2  19035  efgred  19615  dfrhm2  20252  df2idl2  20859  cpmatacl  22217  cpmatmcllem  22219  caucfil  24799  aalioulem6  25849  ajmoi  30106  adjmo  31080  prmidl2  32554  iccllysconn  34236  dfso3  34684  fvineqsnf1  36286  ispridl2  36901  ishlat2  38218  fiinfi  42314  ntrk1k3eqk13  42791  isrnghm  46680  df2idl2rng  46749
  Copyright terms: Public domain W3C validator