Theorem ralrimivv 2877

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)

Hypothesis

Ref	Expression
ralrimivv.1

Assertion

Ref	Expression
ralrimivv

Distinct variable groups:   ,,   ,

Proof of Theorem ralrimivv

Step	Hyp	Ref	Expression
1		ralrimivv.1	. . . 4
2	1	expd 436	. . 3
3	2	ralrimdv 2873	. 2
4	3	ralrimiv 2869	1

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

This theorem is referenced by:  ralrimivva  2878  ralrimdvv  2880  reuind  3303  disjxiun  4449  somo  4839  ssrel2  5098  sorpsscmpl  6591  f1o2ndf1  6908  soxp  6913  smoiso  7052  smo11  7054  fiint  7817  sornom  8678  axdc4lem  8856  zorn2lem6  8902  fpwwe2lem12  9040  fpwwe2lem13  9041  nqereu  9328  genpnnp  9404  receu  10219  lbreu  10518  injresinj  11926  sqrmo  13085  iscatd  15070  isfuncd  15234  symgextf1  16446  lsmsubm  16673  iscmnd  16810  qusabl  16871  dprdsubg  17071  issrngd  17510  quscrng  17888  mamudm  18890  mat1dimcrng  18979  mavmuldm  19052  fitop  19409  tgcl  19471  topbas  19474  ppttop  19508  epttop  19510  restbas  19659  isnrm2  19859  isnrm3  19860  2ndcctbss  19956  txbas  20068  txbasval  20107  txhaus  20148  xkohaus  20154  basqtop  20212  opnfbas  20343  isfild  20359  filfi  20360  neifil  20381  fbasrn  20385  filufint  20421  rnelfmlem  20453  fmfnfmlem3  20457  fmfnfm  20459  blfps  20909  blf  20910  blbas  20933  minveclem3b  21843  aalioulem2  22729  axcontlem9  24275  wlkdvspthlem  24609  frgrawopreglem4  25047  grpodivf  25248  isabloda  25301  ipf  25626  ocsh  26201  adjadj  26855  unopadj2  26857  hmopadj  26858  hmopbdoptHIL  26907  lnopmi  26919  adjlnop  27005  xreceu  27618  esumcocn  28086  mclsax  28929  ghomf1olem  29034  dfon2  29224  nocvxmin  29451  outsideofeu  29781  hilbert1.2  29805  ontopbas  29893  opnrebl2  30139  nn0prpw  30141  fness  30167  tailfb  30195  neificl  30246  metf1o  30248  crngohomfo  30403  smprngopr  30449  ispridlc  30467  prter2  30622  mzpincl  30666  mzpindd  30678  islptre  31625  lmod1  33093  iunconlem2  33735  bnj1384  34088  snatpsubN  35474  pclclN  35615  pclfinN  35624  ltrncnv  35870  cdleme24  36078  cdleme28  36099  cdleme50ltrn  36283  cdleme  36286  ltrnco  36445  cdlemk28-3  36634  diaf11N  36776  dibf11N  36888  dihlsscpre  36961  mapdpg  37433  mapdh9a  37517  mapdh9aOLDN  37518  hdmap14lem6  37603

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