Theorem ralrimivv 3192

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

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

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 3145

This theorem is referenced by:  ralrimivva  3193  ralrimdvv  3195  reuind  3746  disjiund  5058  disjxiun  5065  somo  5512  ssrel2  5661  sorpsscmpl  7462  f1o2ndf1  7820  soxp  7825  smoiso  8001  smo11  8003  fiint  8797  sornom  9701  axdc4lem  9879  zorn2lem6  9925  fpwwe2lem12  10065  fpwwe2lem13  10066  nqereu  10353  genpnnp  10429  receu  11287  lbreu  11593  injresinj  13161  sqrmo  14613  iscatd  16946  isfuncd  17137  0subm  17984  insubm  17985  sursubmefmnd  18063  injsubmefmnd  18064  cycsubm  18347  symgextf1  18551  lsmsubm  18780  iscmnd  18921  qusabl  18987  cycsubmcmn  19010  dprdsubg  19148  issrngd  19634  quscrng  20015  mamudm  21001  mat1dimcrng  21088  mavmuldm  21161  fitop  21510  tgcl  21579  topbas  21582  ppttop  21617  epttop  21619  restbas  21768  isnrm2  21968  isnrm3  21969  2ndcctbss  22065  txbas  22177  txbasval  22216  txhaus  22257  xkohaus  22263  basqtop  22321  opnfbas  22452  isfild  22468  filfi  22469  neifil  22490  fbasrn  22494  filufint  22530  rnelfmlem  22562  fmfnfmlem3  22566  fmfnfm  22568  blfps  23018  blf  23019  blbas  23042  minveclem3b  24033  aalioulem2  24924  axcontlem9  26760  upgrwlkdvdelem  27519  grpodivf  28317  ipf  28492  ocsh  29062  adjadj  29715  unopadj2  29717  hmopadj  29718  hmopbdoptHIL  29767  lnopmi  29779  adjlnop  29865  xreceu  30600  esumcocn  31341  bnj1384  32306  f1resrcmplf1d  32362  mclsax  32818  dfon2  33039  nocvxmin  33250  outsideofeu  33594  hilbert1.2  33618  opnrebl2  33671  nn0prpw  33673  fness  33699  tailfb  33727  ontopbas  33778  neificl  35030  metf1o  35032  crngohomfo  35286  smprngopr  35332  ispridlc  35350  prter2  36019  snatpsubN  36888  pclclN  37029  pclfinN  37038  ltrncnv  37284  cdleme24  37490  cdleme28  37511  cdleme50ltrn  37695  cdleme  37698  ltrnco  37857  cdlemk28-3  38046  diaf11N  38187  dibf11N  38299  dihlsscpre  38372  mapdpg  38844  mapdh9a  38927  mapdh9aOLDN  38928  hdmap14lem6  39011  mzpincl  39338  mzpindd  39350  iunconnlem2  41276  islptre  41907  2reu8i  43319  lmod1  44554