Theorem ralrimivva 2569

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
ralrimivva.1	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )

Assertion

Ref	Expression
ralrimivva	|- ( ph -> A. x e. A A. y e. B ps )

Distinct variable groups:   ph, x, y   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )
2	1	ex 115	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
3	2	ralrimivv 2568	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2158   A.wral 2465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-4 1520  ax-17 1536

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470

This theorem is referenced by:  swopo  4318  sosng  4711  fcof1  5797  fliftfund  5811  isoresbr  5823  isocnv  5825  f1oiso  5840  oveqrspc2v  5915  caovclg  6041  caovcomg  6044  off  6109  caofrss  6121  oprssdmm  6186  dmmpog  6224  fnmpoovd  6230  fmpoco  6231  poxp  6247  f1od2  6250  eroprf  6642  dom2lem  6786  xpf1o  6858  fidifsnid  6885  nnwetri  6929  undiffi  6938  fidcenumlemim  6965  supmoti  7006  supsnti  7018  supisoti  7023  difinfsnlem  7112  nninfwlpor  7186  netap  7267  2omotaplemap  7270  cc2lem  7279  addlocpr  7549  mullocpr  7584  cauappcvgprlemloc  7665  cauappcvgprlemlim  7674  caucvgprlemloc  7688  caucvgprprlemloc  7716  suplocexprlemloc  7734  suplocsrlemb  7819  rereceu  7902  axpre-suploclemres  7914  ltordlem  8453  cju  8932  exbtwnz  10265  frec2uzf1od  10420  frec2uzisod  10421  frecuzrdgrrn  10422  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgg  10430  frecuzrdgsuctlem  10437  seqvalcd  10473  seqovcd  10477  seq3caopr3  10495  seq3caopr2  10496  iseqf1olemqf1o  10507  seq3homo  10524  seq3distr  10527  fimaxq  10821  zfz1isolem1  10834  rsqrmo  11050  climcn2  11331  addcn2  11332  mulcn2  11334  fsum2dlemstep  11456  fisumcom2  11460  cvgratnn  11553  fprodcl2lem  11627  fprod2dlemstep  11644  fprodcom2fi  11648  divalglemeunn  11940  divalglemeuneg  11942  bezoutlemeu  12022  isprm6  12161  pw2dvdseu  12182  crth  12238  eulerthlemh  12245  ennnfonelemim  12439  nninfdclemf1  12467  unbendc  12469  imasaddfnlemg  12753  ercpbl  12769  plusffng  12803  mgmplusf  12804  opifismgmdc  12809  issgrpd  12837  sgrppropd  12838  ismndd  12860  mndpropd  12863  issubmnd  12865  mndinvmod  12868  mhmpropd  12879  idmhm  12882  mhmf1o  12883  issubmd  12887  mndissubm  12888  submid  12890  0mhm  12895  mhmco  12896  grppropd  12915  grpsubf  12976  dfgrp3m  12996  mhmmnd  13011  mhmfmhm  13012  mulgfng  13019  issubg4m  13085  grpissubg  13086  isnsg3  13099  0nsg  13106  nsgid  13107  ghmcmn  13163  ablnsg  13169  imasabl  13171  srgfcl  13225  srglmhm  13245  srgrmhm  13246  subrngringnsg  13425  issubrng2  13430  subrngintm  13432  issubrg2  13461  subrgintm  13463  aprap  13475  islmodd  13482  lmodscaf  13499  lmodprop2d  13537  islssmd  13548  islss4  13571  lsspropdg  13620  issubrgd  13641  dflidl2rng  13670  rnglidlmmgm  13685  tgclb  13861  txbas  14054  txcnp  14067  txcnmpt  14069  cnmpt21  14087  txswaphmeo  14117  isxmetd  14143  isxmet2d  14144  xmettpos  14166  blfvalps  14181  xmetresbl  14236  metss2  14294  comet  14295  bdmet  14298  bdmopn  14300  xmetxp  14303  qtopbasss  14317  elcncf1di  14362  cncfcdm  14365  mulc1cncf  14372  cncfco  14374  dedekindeulemloc  14393  dedekindeu  14397  dedekindicclemloc  14402  dedekindicclemicc  14406  ivthinclemloc  14415  lgseisenlem2  14747  sssneq  15048  exmidsbthrlem  15067  cvgcmp2n  15078  trirec0  15089  apdiff  15093  redc0  15102  reap0  15103  cndcap  15104  neap0mkv  15114