Theorem ralrimivva 2614

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  swopo  4403  sosng  4799  fcof1  5923  fliftfund  5937  isoresbr  5949  isocnv  5951  f1oiso  5966  oveqrspc2v  6044  caovclg  6174  caovcomg  6177  off  6247  caofrss  6266  caofdig  6268  oprssdmm  6333  dmmpog  6373  fnmpoovd  6379  fmpoco  6380  poxp  6396  f1od2  6399  eroprf  6796  dom2lem  6944  xpf1o  7029  fidifsnid  7057  nnwetri  7107  undiffi  7116  fidcenumlemim  7150  supmoti  7191  supsnti  7203  supisoti  7208  difinfsnlem  7297  nninfwlpor  7372  netap  7472  2omotaplemap  7475  cc2lem  7484  addlocpr  7755  mullocpr  7790  cauappcvgprlemloc  7871  cauappcvgprlemlim  7880  caucvgprlemloc  7894  caucvgprprlemloc  7922  suplocexprlemloc  7940  suplocsrlemb  8025  rereceu  8108  axpre-suploclemres  8120  ltordlem  8661  cju  9140  exbtwnz  10509  frec2uzf1od  10667  frec2uzisod  10668  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seqvalcd  10722  seqovcd  10728  seq3caopr3  10752  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemqf1o  10767  seq3homo  10788  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  fimaxq  11090  zfz1isolem1  11103  wrd2ind  11303  rsqrmo  11587  climcn2  11869  addcn2  11870  mulcn2  11872  fsum2dlemstep  11994  fisumcom2  11998  cvgratnn  12091  fprodcl2lem  12165  fprod2dlemstep  12182  fprodcom2fi  12186  divalglemeunn  12481  divalglemeuneg  12483  bezoutlemeu  12577  isprm6  12718  pw2dvdseu  12739  crth  12795  eulerthlemh  12802  4sqlemffi  12968  ennnfonelemim  13044  nninfdclemf1  13072  unbendc  13074  imasaddfnlemg  13396  ercpbl  13413  plusffng  13447  mgmplusf  13448  opifismgmdc  13453  issgrpd  13494  sgrppropd  13495  ismndd  13519  mndpropd  13522  issubmnd  13524  mndinvmod  13527  mhmpropd  13548  idmhm  13551  mhmf1o  13552  issubmd  13556  mndissubm  13557  submid  13559  0mhm  13568  resmhm  13569  resmhm2  13570  resmhm2b  13571  mhmco  13572  grppropd  13599  grpsubf  13661  dfgrp3m  13681  mhmmnd  13702  mhmfmhm  13703  mulgfng  13710  issubg4m  13779  grpissubg  13780  isnsg3  13793  0nsg  13800  nsgid  13801  isghmd  13838  ghmmhm  13839  idghm  13845  ghmnsgima  13854  ghmnsgpreima  13855  ghmf1  13859  kerf1ghm  13860  ghmf1o  13861  ghmcmn  13913  invghm  13915  ablnsg  13920  imasabl  13922  srgfcl  13985  srglmhm  14005  srgrmhm  14006  isrhm2d  14178  subrngringnsg  14218  issubrng2  14223  subrngintm  14225  issubrg2  14254  subrgintm  14256  aprap  14299  islmodd  14306  lmodscaf  14323  lmodprop2d  14361  islssmd  14372  islss4  14395  lsspropdg  14444  issubrgd  14465  dflidl2rng  14494  rnglidlmmgm  14509  expghmap  14620  mulgghm2  14621  znf1o  14664  znidom  14670  tgclb  14788  txbas  14981  txcnp  14994  txcnmpt  14996  cnmpt21  15014  txswaphmeo  15044  isxmetd  15070  isxmet2d  15071  xmettpos  15093  blfvalps  15108  xmetresbl  15163  metss2  15221  comet  15222  bdmet  15225  bdmopn  15227  xmetxp  15230  qtopbasss  15244  elcncf1di  15302  cncfcdm  15305  mulc1cncf  15312  cncfco  15314  dedekindeulemloc  15342  dedekindeu  15346  dedekindicclemloc  15351  dedekindicclemicc  15355  ivthinclemloc  15364  dich0  15375  dvmptfsum  15448  mpodvdsmulf1o  15713  fsumdvdsmul  15714  gausslemma2dlem1f1o  15788  lgseisenlem2  15799  lgsquadlemsfi  15803  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  usgredgreu  16066  uspgredg2vtxeu  16068  uspgredg2v  16071  usgredg2v  16074  vtxedgfi  16139  vtxlpfi  16140  sssneq  16603  exmidsbthrlem  16626  cvgcmp2n  16637  trirec0  16648  apdiff  16652  redc0  16661  reap0  16662  cndcap  16663  neap0mkv  16673