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

Theorem r19.42v 3012
Description: Restricted quantifier version of 19.42v 1775 (see also 19.42 1972). (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v
Distinct variable group:   ,

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 3009 . 2
2 ancom 450 . . 3
32rexbii 2959 . 2
4 ancom 450 . 2
51, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wrex 2808
This theorem is referenced by:  ceqsrexbv  3234  ceqsrex2v  3235  2reuswap  3302  2reu5  3308  rabasiun  4334  iunrab  4377  iunin2  4394  iundif2  4397  reusv2lem4  4656  iunopab  4788  elxp2  5022  cnvuni  5194  xpdifid  5440  elunirn  6163  f1oiso  6247  oprabrexex2  6790  oeeu  7271  trcl  8180  dfac5lem2  8526  axgroth4  9231  rexuz2  11161  4fvwrd4  11822  cshwsexa  12792  divalglem10  14060  divalgb  14062  lsmelval2  17731  tgcmp  19901  hauscmplem  19906  unisngl  20028  xkobval  20087  txtube  20141  txcmplem1  20142  txkgen  20153  xkococnlem  20160  mbfaddlem  22067  mbfsup  22071  elaa  22712  dchrisumlem3  23676  colperpexlem3  24106  midex  24111  ax5seg  24241  usg2spot2nb  25065  usgreg2spot  25067  sumdmdii  27334  2reuswap2  27387  unipreima  27484  fpwrelmapffslem  27555  esumfsup  28076  cvmliftlem15  28743  dfpo2  29184  ellines  29802  cnambfre  30063  rexrabdioph  30727  rmxdioph  30958  expdiophlem1  30963  prmunb2  31191  fourierdlem48  31937  2rmoswap  32189  usgra2pth0  32355  islindeps2  33084  isldepslvec2  33086  bnj168  33785  bnj1398  34090  bj-elsngl  34526  islshpat  34742  lfl1dim  34846  glbconxN  35102  3dim0  35181  2dim  35194  1dimN  35195  islpln5  35259  islvol5  35303  dalem20  35417  lhpex2leN  35737  mapdval4N  37359
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