Theorem ralrimivv 3203

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 421	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜓)))
3	2	ralrimdv 3160	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓))
4	3	ralrimiv 3153	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralrimivva  3205  ralrimdvv  3206  reuind  3710  disjiund  5093  disjxiun  5099  somo  5594  ssrel2  5757  f1resrcmplf1d  7267  sorpsscmpl  7733  resf1extb  7929  f1o2ndf1  8116  soxp  8124  smoiso  8348  smo11  8350  fiint  9296  sornom  10326  axdc4lem  10504  zorn2lem6  10550  fpwwe2lem11  10697  fpwwe2lem12  10698  nqereu  10985  genpnnp  11061  receu  11930  lbreu  12236  injresinj  13894  sqrmo  15385  iscatd  17808  isfuncd  18001  0subm  18974  insubm  18975  sursubmefmnd  19053  injsubmefmnd  19054  cycsubm  19378  symgextf1  19596  lsmsubm  19828  iscmnd  19969  qusabl  20040  cycsubmcmn  20064  dprdsubg  20201  crngrhmfo  20687  issrngd  21073  quscrng  21540  mamudm  22671  mat1dimcrng  22753  mavmuldm  22826  fitop  23179  tgcl  23248  topbas  23251  ppttop  23286  epttop  23288  restbas  23437  isnrm2  23637  isnrm3  23638  2ndcctbss  23735  txbas  23847  txbasval  23886  txhaus  23927  xkohaus  23933  basqtop  23991  opnfbas  24122  isfild  24138  filfi  24139  neifil  24160  fbasrn  24164  filufint  24200  rnelfmlem  24232  fmfnfmlem3  24236  fmfnfm  24238  blfps  24686  blf  24687  blbas  24710  minveclem3b  25710  aalioulem2  26623  nocvxmin  28074  negsprop  28354  axcontlem9  29483  upgrwlkdvdelem  30255  grpodivf  31073  ipf  31248  ocsh  31818  adjadj  32471  unopadj2  32473  hmopadj  32474  hmopbdoptHIL  32523  lnopmi  32535  adjlnop  32621  xreceu  33421  esumcocn  34645  bnj1384  35596  mclsax  36255  dfon2  36476  outsideofeu  36818  hilbert1.2  36842  opnrebl2  37031  nn0prpw  37033  fness  37059  tailfb  37087  ontopbas  37138  mh-inf3f1  37251  neificl  38607  metf1o  38609  crngohomfo  38860  smprngopr  38906  ispridlc  38924  disjdmqsss  39757  disjdmqscossss  39758  eldisjs6  39792  prter2  39858  snatpsubN  40727  pclclN  40868  pclfinN  40877  ltrncnv  41123  cdleme24  41329  cdleme28  41350  cdleme50ltrn  41534  cdleme  41537  ltrnco  41696  cdlemk28-3  41885  diaf11N  42026  dibf11N  42138  dihlsscpre  42211  mapdpg  42683  mapdh9a  42766  mapdh9aOLDN  42767  hdmap14lem6  42850  mzpincl  43683  mzpindd  43695  iunconnlem2  45861  islptre  46553  ormkglobd  47809  fcoresf1  48061  2reu8i  48105  smprngprmrng  49358  lmod1  49526