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

Theorem r2al 3119
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 2035 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 3117 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  wal 1651  wcel 2157  wral 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3093
This theorem is referenced by:  r3al  3120  r2ex  3241  soss  5250  raliunxp  5464  codir  5733  qfto  5734  fununi  6174  dff13  6739  mpt22eqb  7002  tz7.48lem  7774  qliftfun  8069  zorn2lem4  9608  isirred2  19014  cnmpt12  21796  cnmpt22  21803  dchrelbas3  25312  cvmlift2lem12  31806  dfso2  32151  dfpo2  32152  inxpss  34570  inxpss3  34572  isdomn3  38556
  Copyright terms: Public domain W3C validator