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

Theorem r2al 3188
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 1943 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 3136 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062
This theorem is referenced by:  r2ex  3189  r3al  3190  ralcom  3271  nfra2w  3281  moel  3374  raliunxp  5796  codir  6075  qfto  6076  dfpo2  6249  fununi  6577  dff13  7203  mpo2eqb  7489  frpoins3xpg  8073  xpord2indlem  8080  tz7.48lem  8388  qliftfun  8744  zorn2lem4  10440  isirred2  20137  cnmpt12  23034  cnmpt22  23041  dchrelbas3  26602  cvmlift2lem12  33965  dfso2  34384  r2alan  36753  inxpss  36818  inxpss3  36821  isdomn3  41574  iscnrm3lem2  47053  joindm2  47087  meetdm2  47089
  Copyright terms: Public domain W3C validator