Theorem ralrimivv 3205

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  ralrimivva  3207  ralrimdvv  3208  reuind  3718  disjiund  5093  disjxiun  5099  somo  5596  ssrel2  5759  sorpsscmpl  7719  resf1extb  7917  f1o2ndf1  8103  soxp  8111  smoiso  8335  smo11  8337  fiint  9273  sornom  10236  axdc4lem  10414  zorn2lem6  10460  fpwwe2lem11  10601  fpwwe2lem12  10602  nqereu  10889  genpnnp  10965  receu  11834  lbreu  12144  injresinj  13799  sqrmo  15280  iscatd  17707  isfuncd  17900  0subm  18853  insubm  18854  sursubmefmnd  18932  injsubmefmnd  18933  cycsubm  19245  symgextf1  19463  lsmsubm  19695  iscmnd  19836  qusabl  19907  cycsubmcmn  19931  dprdsubg  20068  issrngd  20906  quscrng  21355  mamudm  22457  mat1dimcrng  22539  mavmuldm  22612  fitop  22962  tgcl  23031  topbas  23034  ppttop  23069  epttop  23071  restbas  23220  isnrm2  23420  isnrm3  23421  2ndcctbss  23517  txbas  23629  txbasval  23668  txhaus  23709  xkohaus  23715  basqtop  23773  opnfbas  23904  isfild  23920  filfi  23921  neifil  23942  fbasrn  23946  filufint  23982  rnelfmlem  24014  fmfnfmlem3  24018  fmfnfm  24020  blfps  24468  blf  24469  blbas  24492  minveclem3b  25492  aalioulem2  26399  nocvxmin  27850  negsprop  28130  axcontlem9  29175  upgrwlkdvdelem  29938  grpodivf  30743  ipf  30918  ocsh  31488  adjadj  32141  unopadj2  32143  hmopadj  32144  hmopbdoptHIL  32193  lnopmi  32205  adjlnop  32291  xreceu  33101  esumcocn  34379  bnj1384  35329  f1resrcmplf1d  35383  mclsax  35924  dfon2  36145  outsideofeu  36486  hilbert1.2  36510  opnrebl2  36686  nn0prpw  36688  fness  36714  tailfb  36742  ontopbas  36793  neificl  38257  metf1o  38259  crngohomfo  38510  smprngopr  38556  ispridlc  38574  disjdmqsss  39409  disjdmqscossss  39410  eldisjs6  39444  prter2  39510  snatpsubN  40379  pclclN  40520  pclfinN  40529  ltrncnv  40775  cdleme24  40981  cdleme28  41002  cdleme50ltrn  41186  cdleme  41189  ltrnco  41348  cdlemk28-3  41537  diaf11N  41678  dibf11N  41790  dihlsscpre  41863  mapdpg  42335  mapdh9a  42418  mapdh9aOLDN  42419  hdmap14lem6  42502  mzpincl  43320  mzpindd  43332  iunconnlem2  45515  islptre  46200  ormkglobd  47456  fcoresf1  47668  2reu8i  47712  lmod1  49119