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

Theorem r2al 2936
 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 1866 . 2 (∀𝑦(𝑥𝐴 → (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐵𝜑)))
21r2allem 2934 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1479   ∈ wcel 1988  ∀wral 2909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914 This theorem is referenced by:  r3al  2937  r2ex  3057  soss  5043  raliunxp  5250  codir  5504  qfto  5505  fununi  5952  dff13  6497  mpt22eqb  6754  tz7.48lem  7521  qliftfun  7817  zorn2lem4  9306  isirred2  18682  cnmpt12  21451  cnmpt22  21458  dchrelbas3  24944  cvmlift2lem12  31270  dfso2  31619  dfpo2  31620  isdomn3  37601
 Copyright terms: Public domain W3C validator