Theorem ralrimivva 2443

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 113	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
3	2	ralrimivv 2442	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  swopo  4061  sosng  4431  fcof1  5443  fliftfund  5457  isoresbr  5469  isocnv  5471  f1oiso  5485  caovclg  5673  caovcomg  5676  off  5744  caofrss  5755  fmpt2co  5857  poxp  5873  f1od2  5876  eroprf  6222  dom2lem  6275  nnwetri  6382  supmoti  6406  supsnti  6418  supisoti  6423  addlocpr  6726  mullocpr  6761  cauappcvgprlemloc  6842  cauappcvgprlemlim  6851  caucvgprlemloc  6865  caucvgprprlemloc  6893  rereceu  7055  cju  8038  qbtwnz  9260  frec2uzf1od  9408  frec2uzisod  9409  frecuzrdgrrn  9410  iseqcaopr3  9460  iseqcaopr2  9461  iseqhomo  9468  iseqdistr  9470  rsqrmo  9913  climcn2  10148  addcn2  10149  mulcn2  10151  divalglemeunn  10321  divalglemeuneg  10323  bezoutlemeu  10396  isprm6  10526  pw2dvdseu  10546