Theorem ralrimivva 2444

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

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

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354

This theorem is referenced by:  swopo  4069  sosng  4439  fcof1  5454  fliftfund  5468  isoresbr  5480  isocnv  5482  f1oiso  5496  caovclg  5684  caovcomg  5687  off  5755  caofrss  5766  fmpt2co  5868  poxp  5884  f1od2  5887  eroprf  6265  dom2lem  6319  xpf1o  6385  nnwetri  6436  supmoti  6465  supsnti  6477  supisoti  6482  addlocpr  6788  mullocpr  6823  cauappcvgprlemloc  6904  cauappcvgprlemlim  6913  caucvgprlemloc  6927  caucvgprprlemloc  6955  rereceu  7117  cju  8105  exbtwnz  9337  frec2uzf1od  9488  frec2uzisod  9489  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqoveq  9540  iseqcaopr3  9556  iseqcaopr2  9557  iseqhomo  9565  iseqdistr  9567  rsqrmo  10051  climcn2  10286  addcn2  10287  mulcn2  10289  divalglemeunn  10465  divalglemeuneg  10467  bezoutlemeu  10540  isprm6  10670  pw2dvdseu  10690