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

Theorem r2al 3189
Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.)
Assertion
Ref Expression
r2al (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem r2al
StepHypRef Expression
1 19.21v 1941 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 3188 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  wcel 2115  wral 3126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3131
This theorem is referenced by:  r3al  3190  r2ex  3289  ralcom  3339  raliunxp  5683  codir  5953  qfto  5954  fununi  6402  dff13  6987  mpo2eqb  7257  tz7.48lem  8052  qliftfun  8357  zorn2lem4  9898  isirred2  19429  cnmpt12  22250  cnmpt22  22257  dchrelbas3  25800  cvmlift2lem12  32568  dfso2  32997  dfpo2  32998  inxpss  35609  inxpss3  35611  isdomn3  39945
  Copyright terms: Public domain W3C validator