Theorem ralrimivva 2553

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

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

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 1441  ax-gen 1443  ax-4 1504  ax-17 1520

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-ral 2454

This theorem is referenced by:  swopo  4292  sosng  4685  fcof1  5766  fliftfund  5780  isoresbr  5792  isocnv  5794  f1oiso  5809  oveqrspc2v  5884  caovclg  6009  caovcomg  6012  off  6077  caofrss  6089  oprssdmm  6154  dmmpog  6192  fnmpoovd  6198  fmpoco  6199  poxp  6215  f1od2  6218  eroprf  6610  dom2lem  6754  xpf1o  6826  fidifsnid  6853  nnwetri  6897  undiffi  6906  fidcenumlemim  6933  supmoti  6974  supsnti  6986  supisoti  6991  difinfsnlem  7080  nninfwlpor  7154  cc2lem  7232  addlocpr  7502  mullocpr  7537  cauappcvgprlemloc  7618  cauappcvgprlemlim  7627  caucvgprlemloc  7641  caucvgprprlemloc  7669  suplocexprlemloc  7687  suplocsrlemb  7772  rereceu  7855  axpre-suploclemres  7867  ltordlem  8405  cju  8881  exbtwnz  10211  frec2uzf1od  10366  frec2uzisod  10367  frecuzrdgrrn  10368  frec2uzrdg  10369  frecuzrdgrcl  10370  frecuzrdgsuc  10374  frecuzrdgrclt  10375  frecuzrdgg  10376  frecuzrdgsuctlem  10383  seqvalcd  10419  seqovcd  10423  seq3caopr3  10441  seq3caopr2  10442  iseqf1olemqf1o  10453  seq3homo  10470  seq3distr  10473  fimaxq  10766  zfz1isolem1  10779  rsqrmo  10995  climcn2  11276  addcn2  11277  mulcn2  11279  fsum2dlemstep  11401  fisumcom2  11405  cvgratnn  11498  fprodcl2lem  11572  fprod2dlemstep  11589  fprodcom2fi  11593  divalglemeunn  11884  divalglemeuneg  11886  bezoutlemeu  11966  isprm6  12105  pw2dvdseu  12126  crth  12182  eulerthlemh  12189  ennnfonelemim  12383  nninfdclemf1  12411  unbendc  12413  plusffng  12623  mgmplusf  12624  opifismgmdc  12629  ismndd  12677  mndpropd  12680  mndinvmod  12682  mhmpropd  12693  idmhm  12696  mhmf1o  12697  issubmd  12700  mndissubm  12701  submid  12703  0mhm  12708  mhmco  12709  grppropd  12728  grpsubf  12782  dfgrp3m  12802  mhmmnd  12813  mhmfmhm  12814  mulgfng  12820  tgclb  12944  txbas  13137  txcnp  13150  txcnmpt  13152  cnmpt21  13170  txswaphmeo  13200  isxmetd  13226  isxmet2d  13227  xmettpos  13249  blfvalps  13264  xmetresbl  13319  metss2  13377  comet  13378  bdmet  13381  bdmopn  13383  xmetxp  13386  qtopbasss  13400  elcncf1di  13445  cncffvrn  13448  mulc1cncf  13455  cncfco  13457  dedekindeulemloc  13476  dedekindeu  13480  dedekindicclemloc  13485  dedekindicclemicc  13489  ivthinclemloc  13498  sssneq  14120  exmidsbthrlem  14139  cvgcmp2n  14150  trirec0  14161  apdiff  14165  redc0  14174  reap0  14175