Theorem ralrimivv 3173

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	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))

Assertion

Ref	Expression
ralrimivv	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivv

Step	Hyp	Ref	Expression
1		ralrimivv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
2	1	expd 415	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓)))
3	2	ralrimdv 3130	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓))
4	3	ralrimiv 3123	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3048

This theorem is referenced by:  ralrimivva  3175  ralrimdvv  3176  reuind  3707  disjiund  5080  disjxiun  5086  somo  5561  ssrel2  5724  sorpsscmpl  7667  resf1extb  7864  f1o2ndf1  8052  soxp  8059  smoiso  8282  smo11  8284  fiint  9211  sornom  10168  axdc4lem  10346  zorn2lem6  10392  fpwwe2lem11  10532  fpwwe2lem12  10533  nqereu  10820  genpnnp  10896  receu  11762  lbreu  12072  injresinj  13691  sqrmo  15158  iscatd  17579  isfuncd  17772  0subm  18725  insubm  18726  sursubmefmnd  18804  injsubmefmnd  18805  cycsubm  19114  symgextf1  19333  lsmsubm  19565  iscmnd  19706  qusabl  19777  cycsubmcmn  19801  dprdsubg  19938  issrngd  20770  quscrng  21220  mamudm  22310  mat1dimcrng  22392  mavmuldm  22465  fitop  22815  tgcl  22884  topbas  22887  ppttop  22922  epttop  22924  restbas  23073  isnrm2  23273  isnrm3  23274  2ndcctbss  23370  txbas  23482  txbasval  23521  txhaus  23562  xkohaus  23568  basqtop  23626  opnfbas  23757  isfild  23773  filfi  23774  neifil  23795  fbasrn  23799  filufint  23835  rnelfmlem  23867  fmfnfmlem3  23871  fmfnfm  23873  blfps  24321  blf  24322  blbas  24345  minveclem3b  25355  aalioulem2  26268  nocvxmin  27718  negsprop  27977  axcontlem9  28950  upgrwlkdvdelem  29714  grpodivf  30518  ipf  30693  ocsh  31263  adjadj  31916  unopadj2  31918  hmopadj  31919  hmopbdoptHIL  31968  lnopmi  31980  adjlnop  32066  xreceu  32902  esumcocn  34093  bnj1384  35044  f1resrcmplf1d  35099  mclsax  35613  dfon2  35834  outsideofeu  36175  hilbert1.2  36199  opnrebl2  36365  nn0prpw  36367  fness  36393  tailfb  36421  ontopbas  36472  neificl  37792  metf1o  37794  crngohomfo  38045  smprngopr  38091  ispridlc  38109  disjdmqsss  38899  disjdmqscossss  38900  prter2  38979  snatpsubN  39848  pclclN  39989  pclfinN  39998  ltrncnv  40244  cdleme24  40450  cdleme28  40471  cdleme50ltrn  40655  cdleme  40658  ltrnco  40817  cdlemk28-3  41006  diaf11N  41147  dibf11N  41259  dihlsscpre  41332  mapdpg  41804  mapdh9a  41887  mapdh9aOLDN  41888  hdmap14lem6  41971  mzpincl  42826  mzpindd  42838  iunconnlem2  45026  islptre  45718  ormkglobd  46972  fcoresf1  47168  2reu8i  47212  lmod1  48592