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

Theorem r2al 2845
 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 1930 . 2
21r2allem 2842 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369  wal 1377   wcel 1767  wral 2817 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2822 This theorem is referenced by:  r3al  2847  r3alOLD  2905  r2ex  2990  soss  4824  raliunxp  5148  codir  5393  qfto  5394  fununi  5660  dff13  6165  mpt22eqb  6406  tz7.48lem  7118  qliftfun  7408  zorn2lem4  8891  isirred2  17222  cnmpt12  20036  cnmpt22  20043  dchrelbas3  23379  cvmlift2lem12  28584  dfso2  29110  dfpo2  29111  isdomn3  31093
 Copyright terms: Public domain W3C validator