Theorem ralrimivv 2970

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)

Hypothesis

Ref	Expression
ralrimivv.1	|- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )

Assertion

Ref	Expression
ralrimivv	|- ( ph -> A. x e. A A. y e. B ps )

Distinct variable groups:   x, y, ph   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem ralrimivv

Step	Hyp	Ref	Expression
1		ralrimivv.1	. . . 4 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
2	1	expd 452	. . 3 |- ( ph -> ( x e. A -> ( y e. B -> ps ) ) )
3	2	ralrimdv 2968	. 2 |- ( ph -> ( x e. A -> A. y e. B ps ) )
4	3	ralrimiv 2965	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  ralrimivva  2971  ralrimdvv  2973  reuind  3411  disjiund  4643  disjxiun  4649  disjxiunOLD  4650  somo  5069  ssrel2  5210  sorpsscmpl  6948  f1o2ndf1  7285  soxp  7290  smoiso  7459  smo11  7461  fiint  8237  sornom  9099  axdc4lem  9277  zorn2lem6  9323  fpwwe2lem12  9463  fpwwe2lem13  9464  nqereu  9751  genpnnp  9827  receu  10672  lbreu  10973  injresinj  12589  sqrmo  13992  iscatd  16334  isfuncd  16525  symgextf1  17841  lsmsubm  18068  iscmnd  18205  qusabl  18268  dprdsubg  18423  issrngd  18861  quscrng  19240  mamudm  20194  mat1dimcrng  20283  mavmuldm  20356  fitop  20705  tgcl  20773  topbas  20776  ppttop  20811  epttop  20813  restbas  20962  isnrm2  21162  isnrm3  21163  2ndcctbss  21258  txbas  21370  txbasval  21409  txhaus  21450  xkohaus  21456  basqtop  21514  opnfbas  21646  isfild  21662  filfi  21663  neifil  21684  fbasrn  21688  filufint  21724  rnelfmlem  21756  fmfnfmlem3  21760  fmfnfm  21762  blfps  22211  blf  22212  blbas  22235  minveclem3b  23199  aalioulem2  24088  axcontlem9  25852  upgrwlkdvdelem  26632  grpodivf  27392  ipf  27568  ocsh  28142  adjadj  28795  unopadj2  28797  hmopadj  28798  hmopbdoptHIL  28847  lnopmi  28859  adjlnop  28945  xreceu  29630  esumcocn  30142  bnj1384  31100  mclsax  31466  dfon2  31697  nocvxmin  31894  outsideofeu  32238  hilbert1.2  32262  opnrebl2  32316  nn0prpw  32318  fness  32344  tailfb  32372  ontopbas  32427  neificl  33549  metf1o  33551  crngohomfo  33805  smprngopr  33851  ispridlc  33869  prter2  34166  snatpsubN  35036  pclclN  35177  pclfinN  35186  ltrncnv  35432  cdleme24  35640  cdleme28  35661  cdleme50ltrn  35845  cdleme  35848  ltrnco  36007  cdlemk28-3  36196  diaf11N  36338  dibf11N  36450  dihlsscpre  36523  mapdpg  36995  mapdh9a  37079  mapdh9aOLDN  37080  hdmap14lem6  37165  mzpincl  37297  mzpindd  37309  iunconnlem2  39171  islptre  39851  lmod1  42281