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

Theorem r19.41v 2655
 Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem r19.41v
StepHypRef Expression
1 nfv 1629 . 2
21r19.41 2654 1
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360  wrex 2510 This theorem is referenced by:  r19.42v  2656  3reeanv  2670  reuind  2903  iuncom4  3810  dfiun2g  3833  iunxiun  3882  inuni  4071  reuxfrd  4450  xpiundi  4650  xpiundir  4651  imaco  5084  coiun  5088  abrexco  5618  imaiun  5623  isomin  5686  isoini  5687  oarec  6446  mapsnen  6823  genpass  8513  4sqlem12  12877  imasleval  13317  lsmspsn  15672  metrest  17902  nmoo0  21199  hhcmpl  21609  nmop0  22396  nmfn0  22397  axfelem18  23531  axsegcon  23729  axeuclid  23765  prtlem11  25900  prter2  25915  prter3  25916  diophrex  26021  islshpat  27896  lshpsmreu  27988  islpln5  28413  islvol5  28457  cdlemftr3  29443  dvhb1dimN  29864  dib1dim  30044  mapdpglem3  30554  hdmapglem7a  30809 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-rex 2514
 Copyright terms: Public domain W3C validator