Theorem ralrimivva 2514

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  swopo  4228  sosng  4612  fcof1  5684  fliftfund  5698  isoresbr  5710  isocnv  5712  f1oiso  5727  caovclg  5923  caovcomg  5926  off  5994  caofrss  6006  oprssdmm  6069  dmmpog  6107  fnmpoovd  6112  fmpoco  6113  poxp  6129  f1od2  6132  eroprf  6522  dom2lem  6666  xpf1o  6738  fidifsnid  6765  nnwetri  6804  undiffi  6813  fidcenumlemim  6840  supmoti  6880  supsnti  6892  supisoti  6897  difinfsnlem  6984  addlocpr  7344  mullocpr  7379  cauappcvgprlemloc  7460  cauappcvgprlemlim  7469  caucvgprlemloc  7483  caucvgprprlemloc  7511  suplocexprlemloc  7529  suplocsrlemb  7614  rereceu  7697  axpre-suploclemres  7709  ltordlem  8244  cju  8719  exbtwnz  10028  frec2uzf1od  10179  frec2uzisod  10180  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  seqvalcd  10232  seqovcd  10236  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemqf1o  10266  seq3homo  10283  seq3distr  10286  fimaxq  10573  zfz1isolem1  10583  rsqrmo  10799  climcn2  11078  addcn2  11079  mulcn2  11081  fsum2dlemstep  11203  fisumcom2  11207  cvgratnn  11300  divalglemeunn  11618  divalglemeuneg  11620  bezoutlemeu  11695  isprm6  11825  pw2dvdseu  11846  crth  11900  ennnfonelemim  11937  tgclb  12234  txbas  12427  txcnp  12440  txcnmpt  12442  cnmpt21  12460  txswaphmeo  12490  isxmetd  12516  isxmet2d  12517  xmettpos  12539  blfvalps  12554  xmetresbl  12609  metss2  12667  comet  12668  bdmet  12671  bdmopn  12673  xmetxp  12676  qtopbasss  12690  elcncf1di  12735  cncffvrn  12738  mulc1cncf  12745  cncfco  12747  dedekindeulemloc  12766  dedekindeu  12770  dedekindicclemloc  12775  dedekindicclemicc  12779  ivthinclemloc  12788  exmidsbthrlem  13217  cvgcmp2n  13228