Theorem ralrimdv 2873

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)

Hypothesis

Ref	Expression
ralrimdv.1

Assertion

Ref	Expression
ralrimdv

Distinct variable groups:   ,   ,

Proof of Theorem ralrimdv

Step	Hyp	Ref	Expression
1		ralrimdv.1	. . . 4
2	1	imp 429	. . 3
3	2	ralrimiv 2869	. 2
4	3	ex 434	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralrimdva  2875  ralrimdvaOLD  2876  ralrimivv  2877  wefrc  4878  oneqmin  6640  nneneq  7720  cflm  8651  coflim  8662  isf32lem12  8765  axdc3lem2  8852  zorn2lem7  8903  axpre-sup  9567  infmrcl  10547  zmax  11208  zbtwnre  11209  supxrunb2  11541  fzrevral  11792  islss4  17608  topbas  19474  elcls3  19584  neips  19614  clslp  19649  subbascn  19755  cnpnei  19765  comppfsc  20033  fgss2  20375  fbflim2  20478  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  metcnp3  21043  aalioulem3  22730  brbtwn2  24208  hial0  26019  hial02  26020  ococss  26211  lnopmi  26919  adjlnop  27005  pjss2coi  27083  pj3cor1i  27128  strlem3a  27171  hstrlem3a  27179  mdbr3  27216  mdbr4  27217  dmdmd  27219  dmdbr3  27224  dmdbr4  27225  dmdbr5  27227  ssmd2  27231  mdslmd1i  27248  mdsymlem7  27328  cdj1i  27352  cdj3lem2b  27356  ghomf1olem  29034  lindslinindsimp2  33064  trintALT  33681  lub0N  34914  glb0N  34918  hlrelat2  35127  snatpsubN  35474  pmaple  35485  pclclN  35615  pclfinN  35624  pclfinclN  35674  ltrneq2  35872  trlval2  35888  trlord  36295

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-ral 2812