Theorem ralrimivva 2547

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448

This theorem is referenced by:  swopo  4283  sosng  4676  fcof1  5750  fliftfund  5764  isoresbr  5776  isocnv  5778  f1oiso  5793  caovclg  5990  caovcomg  5993  off  6061  caofrss  6073  oprssdmm  6136  dmmpog  6174  fnmpoovd  6179  fmpoco  6180  poxp  6196  f1od2  6199  eroprf  6590  dom2lem  6734  xpf1o  6806  fidifsnid  6833  nnwetri  6877  undiffi  6886  fidcenumlemim  6913  supmoti  6954  supsnti  6966  supisoti  6971  difinfsnlem  7060  cc2lem  7203  addlocpr  7473  mullocpr  7508  cauappcvgprlemloc  7589  cauappcvgprlemlim  7598  caucvgprlemloc  7612  caucvgprprlemloc  7640  suplocexprlemloc  7658  suplocsrlemb  7743  rereceu  7826  axpre-suploclemres  7838  ltordlem  8376  cju  8852  exbtwnz  10182  frec2uzf1od  10337  frec2uzisod  10338  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  seqvalcd  10390  seqovcd  10394  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemqf1o  10424  seq3homo  10441  seq3distr  10444  fimaxq  10736  zfz1isolem1  10749  rsqrmo  10965  climcn2  11246  addcn2  11247  mulcn2  11249  fsum2dlemstep  11371  fisumcom2  11375  cvgratnn  11468  fprodcl2lem  11542  fprod2dlemstep  11559  fprodcom2fi  11563  divalglemeunn  11854  divalglemeuneg  11856  bezoutlemeu  11936  isprm6  12075  pw2dvdseu  12096  crth  12152  eulerthlemh  12159  ennnfonelemim  12353  nninfdclemf1  12381  unbendc  12383  tgclb  12665  txbas  12858  txcnp  12871  txcnmpt  12873  cnmpt21  12891  txswaphmeo  12921  isxmetd  12947  isxmet2d  12948  xmettpos  12970  blfvalps  12985  xmetresbl  13040  metss2  13098  comet  13099  bdmet  13102  bdmopn  13104  xmetxp  13107  qtopbasss  13121  elcncf1di  13166  cncffvrn  13169  mulc1cncf  13176  cncfco  13178  dedekindeulemloc  13197  dedekindeu  13201  dedekindicclemloc  13206  dedekindicclemicc  13210  ivthinclemloc  13219  sssneq  13842  exmidsbthrlem  13861  cvgcmp2n  13872  trirec0  13883  apdiff  13887  redc0  13896  reap0  13897