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

Theorem reximdv 2931
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
Hypothesis
Ref Expression
reximdv.1
Assertion
Ref Expression
reximdv
Distinct variable group:   ,

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3
21a1d 25 . 2
32reximdvai 2929 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  r19.12  2983  reusv3  4660  fvelima  5925  iunpw  6614  frxp  6910  ssfi  7760  ordtypelem2  7965  wdom2d  8027  xpwdomg  8032  cff1  8659  iunfo  8935  nqereu  9328  reclem3pr  9448  map2psrpr  9508  supsrlem  9509  1re  9616  exprelprel  12528  sswrd  12555  o1lo1  13360  rlimcn1  13411  subcn2  13417  lo1add  13449  lo1mul  13450  pythagtriplem19  14357  vdwnnlem2  14514  ramub2  14532  sylow2alem2  16638  lsmless2x  16665  efgrelexlemb  16768  scmateALT  19014  decpmatmulsumfsupp  19274  pmatcollpw1lem1  19275  pmatcollpw2lem  19278  pm2mpmhmlem1  19319  cpmidpmatlem3  19373  cpmidgsum2  19380  tgcl  19471  neiss  19610  ssnei2  19617  tgcnp  19754  cnpco  19768  cnpresti  19789  lmcnp  19805  hausnei2  19854  1stcrest  19954  nlly2i  19977  llyss  19980  nllyss  19981  reftr  20015  lfinun  20026  txcnpi  20109  txcmplem1  20142  tx1stc  20151  nrmr0reg  20250  fbssfi  20338  fbfinnfr  20342  fgcl  20379  ufinffr  20430  elfm2  20449  fmfnfmlem1  20455  fmco  20462  fbflim2  20478  flffbas  20496  flftg  20497  cnpflf2  20501  alexsubALT  20551  cnextcn  20567  isucn2  20782  ucnima  20784  blssexps  20929  blssex  20930  mopni3  20997  neibl  21004  metss  21011  metcnp3  21043  cfilucfilOLD  21072  cfilucfil  21073  metustblOLD  21083  metustbl  21084  metutopOLD  21085  psmetutop  21086  rescncf  21401  lebnum  21464  xlebnum  21465  lebnumii  21466  lmmbr  21697  fgcfil  21710  ovolsslem  21895  ovolunlem1  21908  ovoliunnul  21918  itgcn  22249  ellimc3  22283  c1lip3  22400  itgsubstlem  22449  plyss  22596  ulmclm  22782  ulmcau  22790  ulmcn  22794  rlimcxp  23303  chtppilimlem2  23659  chtppilim  23660  midex  24111  usgranloop0  24380  usgra2edg  24382  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  vdusgra0nedg  24908  usgravd0nedg  24918  3cyclfrgrarn2  25014  vdn0frgrav2  25023  vdgn0frgrav2  25024  frgrawopreg1  25050  frgrawopreg2  25051  isgrpo  25198  opidonOLD  25324  rngmgmbs4  25419  xrge0infss  27580  tpr2rico  27894  esumpcvgval  28084  conpcon  28680  cvmliftlem15  28743  cvmlift2lem10  28757  fnessref  30175  fdc1  30239  sstotbnd3  30272  totbndss  30273  heibor1lem  30305  heibor1  30306  fiphp3d  30753  pell1qrss14  30804  ssfiunibd  31509  infrglb  31584  climrec  31609  islptre  31625  lptre2pt  31646  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem27  31809  stoweidlem29  31811  stoweidlem35  31817  stoweidlem48  31830  stoweidlem62  31844  fourierdlem48  31937  fourierdlem64  31953  fourierdlem65  31954  fourierdlem71  31960  fourierdlem73  31962  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  afvelima  32252  usgvincvad  32404  usgvincvadALT  32407  pgrpgt2nabl  32959  lvoli2  35305  paddss2  35542  lhpexle1lem  35731  lhpexle2lem  35733  dvhdimlem  37171  dvh3dim3N  37176  mapdh9a  37517  hdmap11lem2  37572
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