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

Theorem r2al 3195
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 1939 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 3142 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wcel 2108  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  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062
This theorem is referenced by:  r2ex  3196  r3al  3197  ralcom  3289  nfra2w  3299  moel  3402  raliunxp  5850  codir  6140  qfto  6141  dfpo2  6316  fununi  6641  dff13  7275  mpo2eqb  7565  frpoins3xpg  8165  xpord2indlem  8172  tz7.48lem  8481  qliftfun  8842  zorn2lem4  10539  isirred2  20421  isdomn3  20715  cnmpt12  23675  cnmpt22  23682  dchrelbas3  27282  cvmlift2lem12  35319  dfso2  35755  r2alan  38250  inxpss  38312  inxpss3  38315  dfac5prim  45007  iscnrm3lem2  48832  joindm2  48865  meetdm2  48867
  Copyright terms: Public domain W3C validator