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

Theorem r19.41v 3009
Description: Restricted quantifier version 19.41v 1771. Version of r19.41 3010 with a dv condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduced dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
Assertion
Ref Expression
r19.41v
Distinct variable group:   ,

Proof of Theorem r19.41v
StepHypRef Expression
1 anass 649 . . . 4
21exbii 1667 . . 3
3 19.41v 1771 . . 3
42, 3bitr3i 251 . 2
5 df-rex 2813 . 2
6 df-rex 2813 . . 3
76anbi1i 695 . 2
84, 5, 73bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  r19.41vv  3011  r19.42v  3012  3reeanv  3026  reuind  3303  iuncom4  4338  dfiun2g  4362  iunxiun  4413  inuni  4614  reuxfrd  4677  xpiundi  5059  xpiundir  5060  imaco  5517  coiun  5522  abrexco  6156  imaiun  6157  isomin  6233  isoini  6234  oarec  7230  mapsnen  7613  genpass  9408  4fvwrd4  11822  4sqlem12  14474  imasleval  14938  lsmspsn  17730  utoptop  20737  metrest  21027  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  metuel2  21082  istrkg2ld  23858  axsegcon  24230  usgreg2spot  25067  nmoo0  25706  hhcmpl  26117  nmop0  26905  nmfn0  26906  reuxfr4d  27389  rexunirn  27390  ordtconlem1  27906  dya2icoseg2  28249  dya2iocnei  28253  nofulllem5  29466  rabiun  30036  iundif1  30037  ismblfin  30055  prtlem11  30607  prter2  30622  prter3  30623  diophrex  30709  islshpat  34742  lshpsmreu  34834  islpln5  35259  islvol5  35303  cdlemftr3  36291  dvhb1dimN  36712  dib1dim  36892  mapdpglem3  37402  hdmapglem7a  37657
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  ax-6 1747
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813
  Copyright terms: Public domain W3C validator