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

Theorem r19.23v 2621
 Description: Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.23v
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem r19.23v
StepHypRef Expression
1 nfv 1629 . 2
21r19.23 2620 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178  wral 2509  wrex 2510 This theorem is referenced by:  uniiunlem  3181  dfiin2g  3834  iunss  3841  ralxfr2d  4441  reliun  4713  funimass4  5425  ralrnmpt2  5810  kmlem12  7671  fimaxre3  9583  gcdcllem1  12564  vdwmc2  12900  iunocv  16413  ovolgelb  18671  dyadmax  18785  itg2leub  18921  nmoubi  21180  nmopub  22318  nmfnleub  22335  untuni  23226  dfpo2  23282  mptelee  23697  heibor1lem  25699  ralxpxfr2d  25926  islindf4  26474  ispsubsp2  28624  pmapglbx  28647 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
 Copyright terms: Public domain W3C validator