Theorem ralrimivva 2632

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  swopo  4453  sosng  4850  fcof1  5992  fliftfund  6006  isoresbr  6018  isocnv  6020  f1oiso  6035  oveqrspc2v  6115  caovclg  6245  caovcomg  6248  off  6319  caofrss  6338  caofdig  6340  oprssdmm  6409  dmmpog  6449  fnmpoovd  6455  fmpoco  6456  poxp  6472  f1od2  6475  suppofss1dcl  6508  suppofss2dcl  6509  eroprf  6906  dom2lem  7062  xpf1o  7148  fidifsnid  7177  nnwetri  7227  undiffi  7236  fidcenumlemim  7274  supmoti  7339  supsnti  7351  supisoti  7356  difinfsnlem  7445  nninfwlpor  7520  netap  7626  2omotaplemap  7629  cc2lem  7638  addlocpr  7909  mullocpr  7944  cauappcvgprlemloc  8025  cauappcvgprlemlim  8034  caucvgprlemloc  8048  caucvgprprlemloc  8076  suplocexprlemloc  8094  suplocsrlemb  8179  rereceu  8262  axpre-suploclemres  8274  ltordlem  8817  cju  9299  exbtwnz  10702  frec2uzf1od  10864  frec2uzisod  10865  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgsuctlem  10881  seqvalcd  10919  seqovcd  10925  seq3caopr3  10949  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemqf1o  10964  seq3homo  10985  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  fimaxq  11292  zfz1isolem1  11314  wrd2ind  11517  rsqrmo  11815  climcn2  12100  addcn2  12101  mulcn2  12103  fsum2dlemstep  12226  fisumcom2  12230  cvgratnn  12323  fprodcl2lem  12397  fprod2dlemstep  12414  fprodcom2fi  12418  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemeu  12809  isprm6  12951  pwbdvdseu  12972  crth  13031  eulerthlemh  13038  4sqlemffi  13204  ennnfonelemim  13373  nninfdclemf1  13401  unbendc  13403  imasaddfnlemg  13694  ercpbl  13711  plusffng  13744  mgmplusf  13745  opifismgmdc  13750  issgrpd  13786  sgrppropd  13787  ismndd  13809  mndpropd  13812  issubmnd  13814  mndinvmod  13817  mhmpropd  13832  idmhm  13835  mhmf1o  13836  issubmd  13840  mndissubm  13841  submid  13843  0mhm  13852  resmhm  13853  resmhm2  13854  resmhm2b  13855  mhmco  13856  grppropd  13881  grpsubf  13943  dfgrp3m  13963  mhmmnd  13978  mhmfmhm  13979  mulgfng  13986  issubg4m  14055  grpissubg  14056  isnsg3  14069  0nsg  14076  nsgid  14077  isghmd  14114  ghmmhm  14115  idghm  14121  ghmnsgima  14130  ghmnsgpreima  14131  ghmf1  14135  kerf1ghm  14136  ghmf1o  14137  cntzsgrpcl  14167  cntzsubm  14170  cntrsubgnsg  14175  cmnsubm  14202  ghmcmn  14221  invghm  14223  ablnsg  14228  imasabl  14230  gsum2d2fi  14274  gsumcom2fi  14275  srgfcl  14384  srglmhm  14404  srgrmhm  14405  isrhm2d  14581  subrngringnsg  14622  issubrng2  14627  subrngintm  14629  issubrg2  14658  subrgintm  14660  aprap  14707  aprlring  14709  islmodd  14738  lmodscaf  14756  lmodprop2d  14794  islssmd  14805  islss4  14828  lsspropdg  14877  issubrgd  14898  dflidl2rng  14927  rnglidlmmgm  14942  expghmap  15051  mulgghm2  15052  znf1o  15095  znidom  15101  issubassa2  15144  tgclb  15291  txbas  15484  txcnp  15497  txcnmpt  15499  cnmpt21  15517  txswaphmeo  15547  isxmetd  15573  isxmet2d  15574  xmettpos  15596  blfvalps  15611  xmetresbl  15666  metss2  15724  comet  15725  bdmet  15728  bdmopn  15730  xmetxp  15733  qtopbasss  15747  elcncf1di  15805  cncfcdm  15808  mulc1cncf  15815  cncfco  15817  dedekindeulemloc  15845  dedekindeu  15849  dedekindicclemloc  15854  dedekindicclemicc  15858  ivthinclemloc  15867  dich0  15878  dvmptfsum  15951  mpodvdsmulf1o  16284  fsumdvdsmul  16285  gausslemma2dlem1f1o  16384  lgseisenlem2  16395  lgsquadlemsfi  16399  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  usgredgreu  16662  uspgredg2vtxeu  16664  uspgredg2v  16667  usgredg2v  16670  vtxedgfi  16735  vtxlpfi  16736  dichmul0or  16965  sssneq  17237  exmidsbthrlem  17273  cvgcmp2n  17288  trirec0  17300  apdiff  17304  redc0  17314  reap0  17315  cndcap  17316  neap0mkv  17326