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 1871. 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 275 1 (∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 ∧ ∀𝑥𝐴𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062
This theorem is referenced by:  fununi  6641  tz7.48lem  8481  isffth2  17963  ispos2  18361  issgrpv  18734  issgrpn0  18735  isnsg2  19174  efgred  19766  isrnghm  20441  dfrhm2  20474  df2idl2rng  21266  cpmatacl  22722  cpmatmcllem  22724  caucfil  25317  aalioulem6  26379  ajmoi  30877  adjmo  31851  prmidl2  33469  iccllysconn  35255  dfso3  35720  fvineqsnf1  37411  ispridl2  38045  ishlat2  39354  fiinfi  43586  ntrk1k3eqk13  44063
  Copyright terms: Public domain W3C validator