Theorem ralrimivv 3155

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  ralrimivva  3156  ralrimdvv  3158  reuind  3692  disjiund  5020  disjxiun  5027  somo  5474  ssrel2  5623  sorpsscmpl  7440  f1o2ndf1  7801  soxp  7806  smoiso  7982  smo11  7984  fiint  8779  sornom  9688  axdc4lem  9866  zorn2lem6  9912  fpwwe2lem12  10052  fpwwe2lem13  10053  nqereu  10340  genpnnp  10416  receu  11274  lbreu  11578  injresinj  13153  sqrmo  14603  iscatd  16936  isfuncd  17127  0subm  17974  insubm  17975  sursubmefmnd  18053  injsubmefmnd  18054  cycsubm  18337  symgextf1  18541  lsmsubm  18770  iscmnd  18911  qusabl  18978  cycsubmcmn  19001  dprdsubg  19139  issrngd  19625  quscrng  20006  mamudm  20995  mat1dimcrng  21082  mavmuldm  21155  fitop  21505  tgcl  21574  topbas  21577  ppttop  21612  epttop  21614  restbas  21763  isnrm2  21963  isnrm3  21964  2ndcctbss  22060  txbas  22172  txbasval  22211  txhaus  22252  xkohaus  22258  basqtop  22316  opnfbas  22447  isfild  22463  filfi  22464  neifil  22485  fbasrn  22489  filufint  22525  rnelfmlem  22557  fmfnfmlem3  22561  fmfnfm  22563  blfps  23013  blf  23014  blbas  23037  minveclem3b  24032  aalioulem2  24929  axcontlem9  26766  upgrwlkdvdelem  27525  grpodivf  28321  ipf  28496  ocsh  29066  adjadj  29719  unopadj2  29721  hmopadj  29722  hmopbdoptHIL  29771  lnopmi  29783  adjlnop  29869  xreceu  30624  esumcocn  31449  bnj1384  32414  f1resrcmplf1d  32470  mclsax  32929  dfon2  33150  nocvxmin  33361  outsideofeu  33705  hilbert1.2  33729  opnrebl2  33782  nn0prpw  33784  fness  33810  tailfb  33838  ontopbas  33889  neificl  35191  metf1o  35193  crngohomfo  35444  smprngopr  35490  ispridlc  35508  prter2  36177  snatpsubN  37046  pclclN  37187  pclfinN  37196  ltrncnv  37442  cdleme24  37648  cdleme28  37669  cdleme50ltrn  37853  cdleme  37856  ltrnco  38015  cdlemk28-3  38204  diaf11N  38345  dibf11N  38457  dihlsscpre  38530  mapdpg  39002  mapdh9a  39085  mapdh9aOLDN  39086  hdmap14lem6  39169  mzpincl  39675  mzpindd  39687  iunconnlem2  41641  islptre  42261  2reu8i  43669  lmod1  44901