Theorem ralrimivv 3190

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3138

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 209  df-an 399  df-ral 3143

This theorem is referenced by:  ralrimivva  3191  ralrimdvv  3193  reuind  3744  disjiund  5056  disjxiun  5063  somo  5510  ssrel2  5659  sorpsscmpl  7460  f1o2ndf1  7818  soxp  7823  smoiso  7999  smo11  8001  fiint  8795  sornom  9699  axdc4lem  9877  zorn2lem6  9923  fpwwe2lem12  10063  fpwwe2lem13  10064  nqereu  10351  genpnnp  10427  receu  11285  lbreu  11591  injresinj  13159  sqrmo  14611  iscatd  16944  isfuncd  17135  0subm  17982  insubm  17983  sursubmefmnd  18061  injsubmefmnd  18062  cycsubm  18345  symgextf1  18549  lsmsubm  18778  iscmnd  18919  qusabl  18985  cycsubmcmn  19008  dprdsubg  19146  issrngd  19632  quscrng  20013  mamudm  20999  mat1dimcrng  21086  mavmuldm  21159  fitop  21508  tgcl  21577  topbas  21580  ppttop  21615  epttop  21617  restbas  21766  isnrm2  21966  isnrm3  21967  2ndcctbss  22063  txbas  22175  txbasval  22214  txhaus  22255  xkohaus  22261  basqtop  22319  opnfbas  22450  isfild  22466  filfi  22467  neifil  22488  fbasrn  22492  filufint  22528  rnelfmlem  22560  fmfnfmlem3  22564  fmfnfm  22566  blfps  23016  blf  23017  blbas  23040  minveclem3b  24031  aalioulem2  24922  axcontlem9  26758  upgrwlkdvdelem  27517  grpodivf  28315  ipf  28490  ocsh  29060  adjadj  29713  unopadj2  29715  hmopadj  29716  hmopbdoptHIL  29765  lnopmi  29777  adjlnop  29863  xreceu  30598  esumcocn  31339  bnj1384  32304  f1resrcmplf1d  32360  mclsax  32816  dfon2  33037  nocvxmin  33248  outsideofeu  33592  hilbert1.2  33616  opnrebl2  33669  nn0prpw  33671  fness  33697  tailfb  33725  ontopbas  33776  neificl  35043  metf1o  35045  crngohomfo  35299  smprngopr  35345  ispridlc  35363  prter2  36032  snatpsubN  36901  pclclN  37042  pclfinN  37051  ltrncnv  37297  cdleme24  37503  cdleme28  37524  cdleme50ltrn  37708  cdleme  37711  ltrnco  37870  cdlemk28-3  38059  diaf11N  38200  dibf11N  38312  dihlsscpre  38385  mapdpg  38857  mapdh9a  38940  mapdh9aOLDN  38941  hdmap14lem6  39024  mzpincl  39351  mzpindd  39363  iunconnlem2  41289  islptre  41920  2reu8i  43332  lmod1  44567