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

Theorem r19.23v 2937
 Description: Restricted quantifier version of 19.23v 1760. Version of r19.23 2936 with a dv condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Assertion
Ref Expression
r19.23v
Distinct variable group:   ,

Proof of Theorem r19.23v
StepHypRef Expression
1 con34b 292 . . 3
21ralbii 2888 . 2
3 r19.21v 2862 . 2
4 dfrex2 2908 . . . 4
54imbi1i 325 . . 3
6 con1b 333 . . 3
75, 6bitr2i 250 . 2
82, 3, 73bitri 271 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  <->wb 184  A.wral 2807  E.wrex 2808 This theorem is referenced by:  rexlimiv  2943  ralxpxfr2d  3224  uniiunlem  3587  dfiin2g  4363  iunss  4371  ralxfr2d  4668  ssrel2  5098  reliun  5128  funimass4  5924  ralrnmpt2  6417  kmlem12  8562  fimaxre3  10517  gcdcllem1  14149  vdwmc2  14497  iunocv  18712  islindf4  18873  ovolgelb  21891  dyadmax  22007  itg2leub  22141  mptelee  24198  nmoubi  25687  nmopub  26827  nmfnleub  26844  sigaclcu2  28120  untuni  29081  dfpo2  29184  heibor1lem  30305  2reu4a  32194  ispsubsp2  35470  pmapglbx  35493 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  df-rex 2813
 Copyright terms: Public domain W3C validator