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

Theorem r2al 2835
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:   ,   ,

Proof of Theorem r2al
StepHypRef Expression
1 19.21v 1729 . 2
21r2allem 2832 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  e.wcel 1818  A.wral 2807
This theorem is referenced by:  r3al  2837  r3alOLD  2895  r2ex  2980  soss  4823  raliunxp  5147  codir  5392  qfto  5393  fununi  5659  dff13  6166  mpt22eqb  6411  tz7.48lem  7125  qliftfun  7415  zorn2lem4  8900  isirred2  17350  cnmpt12  20168  cnmpt22  20175  dchrelbas3  23513  cvmlift2lem12  28759  dfso2  29183  dfpo2  29184  isdomn3  31164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812
  Copyright terms: Public domain W3C validator