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

Theorem ralrimdv 2752
 Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
ralrimdv.1
Assertion
Ref Expression
ralrimdv
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem ralrimdv
StepHypRef Expression
1 nfv 1626 . 2
2 nfv 1626 . 2
3 ralrimdv.1 . 2
41, 2, 3ralrimd 2751 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 1721  wral 2663 This theorem is referenced by:  ralrimdva  2753  ralrimivv  2754  wefrc  4531  oneqmin  4739  tfrlem1  6586  abianfp  6666  nneneq  7240  cflm  8077  coflim  8088  isf32lem12  8191  axdc3lem2  8278  zorn2lem7  8329  axpre-sup  8991  infmrcl  9933  zmax  10517  zbtwnre  10518  supxrunb2  10845  fzrevral  11075  islss4  15979  topbas  16974  elcls3  17084  neips  17114  clslp  17148  subbascn  17254  cnpnei  17264  fgss2  17841  fbflim2  17944  alexsubALTlem3  18015  alexsubALTlem4  18016  alexsubALT  18017  metcnp3  18474  aalioulem3  20132  hial0  22466  hial02  22467  ococss  22657  lnopmi  23365  adjlnop  23451  pjss2coi  23529  pj3cor1i  23574  strlem3a  23617  hstrlem3a  23625  mdbr3  23662  mdbr4  23663  dmdmd  23665  dmdbr3  23670  dmdbr4  23671  dmdbr5  23673  ssmd2  23677  mdslmd1i  23694  mdsymlem7  23774  cdj1i  23798  cdj3lem2b  23802  ghomf1olem  24898  brbtwn2  25572  comppfsc  26094  trintALT  28350  lub0N  29320  hlrelat2  29533  snatpsubN  29880  pmaple  29891  pclclN  30021  pclfinN  30030  pclfinclN  30080  ltrneq2  30278  trlval2  30293  trlord  30699 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757 This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2668
 Copyright terms: Public domain W3C validator