Theorem ralrimivva 2626

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 2625	1 |- ( ph -> A. x e. A A. y e. B ps )

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  swopo  4433  sosng  4830  fcof1  5964  fliftfund  5978  isoresbr  5990  isocnv  5992  f1oiso  6007  oveqrspc2v  6087  caovclg  6217  caovcomg  6220  off  6290  caofrss  6309  caofdig  6311  oprssdmm  6380  dmmpog  6420  fnmpoovd  6426  fmpoco  6427  poxp  6443  f1od2  6446  suppofss1dcl  6479  suppofss2dcl  6480  eroprf  6877  dom2lem  7026  xpf1o  7112  fidifsnid  7141  nnwetri  7191  undiffi  7200  fidcenumlemim  7237  supmoti  7299  supsnti  7311  supisoti  7316  difinfsnlem  7405  nninfwlpor  7480  netap  7586  2omotaplemap  7589  cc2lem  7598  addlocpr  7869  mullocpr  7904  cauappcvgprlemloc  7985  cauappcvgprlemlim  7994  caucvgprlemloc  8008  caucvgprprlemloc  8036  suplocexprlemloc  8054  suplocsrlemb  8139  rereceu  8222  axpre-suploclemres  8234  ltordlem  8776  cju  9257  exbtwnz  10639  frec2uzf1od  10797  frec2uzisod  10798  frecuzrdgrrn  10799  frec2uzrdg  10800  frecuzrdgrcl  10801  frecuzrdgsuc  10805  frecuzrdgrclt  10806  frecuzrdgg  10807  frecuzrdgsuctlem  10814  seqvalcd  10852  seqovcd  10858  seq3caopr3  10882  seq3caopr2  10884  seqcaopr2g  10885  iseqf1olemqf1o  10897  seq3homo  10918  seqhomog  10921  seqfeq4g  10922  seq3distr  10923  fimaxq  11224  zfz1isolem1  11242  wrd2ind  11445  rsqrmo  11743  climcn2  12025  addcn2  12026  mulcn2  12028  fsum2dlemstep  12151  fisumcom2  12155  cvgratnn  12248  fprodcl2lem  12322  fprod2dlemstep  12339  fprodcom2fi  12343  divalglemeunn  12638  divalglemeuneg  12640  bezoutlemeu  12734  isprm6  12875  pw2dvdseu  12896  crth  12952  eulerthlemh  12959  4sqlemffi  13125  ennnfonelemim  13265  nninfdclemf1  13293  unbendc  13295  imasaddfnlemg  13584  ercpbl  13601  plusffng  13634  mgmplusf  13635  opifismgmdc  13640  issgrpd  13676  sgrppropd  13677  ismndd  13699  mndpropd  13702  issubmnd  13704  mndinvmod  13707  mhmpropd  13722  idmhm  13725  mhmf1o  13726  issubmd  13730  mndissubm  13731  submid  13733  0mhm  13742  resmhm  13743  resmhm2  13744  resmhm2b  13745  mhmco  13746  grppropd  13771  grpsubf  13833  dfgrp3m  13853  mhmmnd  13868  mhmfmhm  13869  mulgfng  13876  issubg4m  13945  grpissubg  13946  isnsg3  13959  0nsg  13966  nsgid  13967  isghmd  14004  ghmmhm  14005  idghm  14011  ghmnsgima  14020  ghmnsgpreima  14021  ghmf1  14025  kerf1ghm  14026  ghmf1o  14027  cmnsubm  14061  ghmcmn  14080  invghm  14082  ablnsg  14087  imasabl  14089  srgfcl  14223  srglmhm  14243  srgrmhm  14244  isrhm2d  14417  subrngringnsg  14458  issubrng2  14463  subrngintm  14465  issubrg2  14494  subrgintm  14496  aprap  14543  aprlring  14545  islmodd  14574  lmodscaf  14591  lmodprop2d  14629  islssmd  14640  islss4  14663  lsspropdg  14712  issubrgd  14733  dflidl2rng  14762  rnglidlmmgm  14777  expghmap  14886  mulgghm2  14887  znf1o  14930  znidom  14936  tgclb  15061  txbas  15254  txcnp  15267  txcnmpt  15269  cnmpt21  15287  txswaphmeo  15317  isxmetd  15343  isxmet2d  15344  xmettpos  15366  blfvalps  15381  xmetresbl  15436  metss2  15494  comet  15495  bdmet  15498  bdmopn  15500  xmetxp  15503  qtopbasss  15517  elcncf1di  15575  cncfcdm  15578  mulc1cncf  15585  cncfco  15587  dedekindeulemloc  15615  dedekindeu  15619  dedekindicclemloc  15624  dedekindicclemicc  15628  ivthinclemloc  15637  dich0  15648  dvmptfsum  15721  mpodvdsmulf1o  15989  fsumdvdsmul  15990  gausslemma2dlem1f1o  16064  lgseisenlem2  16075  lgsquadlemsfi  16079  lgsquadlem1  16081  lgsquadlem2  16082  lgsquadlem3  16083  usgredgreu  16342  uspgredg2vtxeu  16344  uspgredg2v  16347  usgredg2v  16350  vtxedgfi  16415  vtxlpfi  16416  dichmul0or  16645  sssneq  16917  exmidsbthrlem  16943  cvgcmp2n  16958  trirec0  16969  apdiff  16973  redc0  16983  reap0  16984  cndcap  16985  neap0mkv  16995