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

Theorem r2al 3185
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 1935 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 3132 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1532  wcel 2099  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3052
This theorem is referenced by:  r2ex  3186  r3al  3187  ralcom  3277  nfra2w  3287  moel  3386  raliunxp  5846  codir  6132  qfto  6133  dfpo2  6307  fununi  6634  dff13  7270  mpo2eqb  7558  frpoins3xpg  8154  xpord2indlem  8161  tz7.48lem  8471  qliftfun  8831  zorn2lem4  10542  isirred2  20403  isdomn3  20693  cnmpt12  23662  cnmpt22  23669  dchrelbas3  27267  cvmlift2lem12  35142  dfso2  35577  r2alan  37947  inxpss  38009  inxpss3  38012  iscnrm3lem2  48268  joindm2  48302  meetdm2  48304
  Copyright terms: Public domain W3C validator