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

Theorem r19.21v 2862
Description: Restricted quantifier version of 19.21v 1729. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.)
Assertion
Ref Expression
r19.21v
Distinct variable group:   ,

Proof of Theorem r19.21v
StepHypRef Expression
1 bi2.04 361 . . . 4
21albii 1640 . . 3
3 19.21v 1729 . . 3
42, 3bitri 249 . 2
5 df-ral 2812 . 2
6 df-ral 2812 . . 3
76imbi2i 312 . 2
84, 5, 73bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  A.wral 2807
This theorem is referenced by:  r19.23v  2937  r19.32v  3003  rmo4  3292  2reu5lem3  3307  ra4v  3423  rmo3  3429  dftr5  4548  reusv3  4660  tfinds2  6698  tfinds3  6699  tfrlem1  7064  tfr3  7087  oeordi  7255  ordiso2  7961  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  dfac12lem3  8546  ttukeylem5  8914  ttukeylem6  8915  fpwwe2lem8  9036  grudomon  9216  raluz2  11159  ndvdssub  14065  gcdcllem1  14149  acsfn2  15060  pgpfac1  17131  pgpfac  17135  isdomn2  17948  islindf4  18873  isclo2  19589  1stccn  19964  kgencn  20057  txflf  20507  fclsopn  20515  nn0min  27611  rdgprc  29227  wfr3g  29342  bpolycl  29814  heicant  30049  filnetlem4  30199  2rexrsb  32176  bnj580  33971  bnj852  33979
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-ex 1613  df-ral 2812
  Copyright terms: Public domain W3C validator