Theorem ralrimivv 3176

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3050

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3051

This theorem is referenced by:  ralrimivva  3178  ralrimdvv  3179  reuind  3710  disjiund  5088  disjxiun  5094  somo  5570  ssrel2  5733  sorpsscmpl  7679  resf1extb  7876  f1o2ndf1  8064  soxp  8071  smoiso  8294  smo11  8296  fiint  9229  sornom  10189  axdc4lem  10367  zorn2lem6  10413  fpwwe2lem11  10554  fpwwe2lem12  10555  nqereu  10842  genpnnp  10918  receu  11784  lbreu  12094  injresinj  13709  sqrmo  15176  iscatd  17598  isfuncd  17791  0subm  18744  insubm  18745  sursubmefmnd  18823  injsubmefmnd  18824  cycsubm  19133  symgextf1  19352  lsmsubm  19584  iscmnd  19725  qusabl  19796  cycsubmcmn  19820  dprdsubg  19957  issrngd  20790  quscrng  21240  mamudm  22341  mat1dimcrng  22423  mavmuldm  22496  fitop  22846  tgcl  22915  topbas  22918  ppttop  22953  epttop  22955  restbas  23104  isnrm2  23304  isnrm3  23305  2ndcctbss  23401  txbas  23513  txbasval  23552  txhaus  23593  xkohaus  23599  basqtop  23657  opnfbas  23788  isfild  23804  filfi  23805  neifil  23826  fbasrn  23830  filufint  23866  rnelfmlem  23898  fmfnfmlem3  23902  fmfnfm  23904  blfps  24352  blf  24353  blbas  24376  minveclem3b  25386  aalioulem2  26299  nocvxmin  27753  negsprop  28015  axcontlem9  29026  upgrwlkdvdelem  29790  grpodivf  30594  ipf  30769  ocsh  31339  adjadj  31992  unopadj2  31994  hmopadj  31995  hmopbdoptHIL  32044  lnopmi  32056  adjlnop  32142  xreceu  32982  esumcocn  34216  bnj1384  35167  f1resrcmplf1d  35222  mclsax  35742  dfon2  35963  outsideofeu  36304  hilbert1.2  36328  opnrebl2  36494  nn0prpw  36496  fness  36522  tailfb  36550  ontopbas  36601  neificl  37923  metf1o  37925  crngohomfo  38176  smprngopr  38222  ispridlc  38240  disjdmqsss  39075  disjdmqscossss  39076  eldisjs6  39110  prter2  39176  snatpsubN  40045  pclclN  40186  pclfinN  40195  ltrncnv  40441  cdleme24  40647  cdleme28  40668  cdleme50ltrn  40852  cdleme  40855  ltrnco  41014  cdlemk28-3  41203  diaf11N  41344  dibf11N  41456  dihlsscpre  41529  mapdpg  42001  mapdh9a  42084  mapdh9aOLDN  42085  hdmap14lem6  42168  mzpincl  43013  mzpindd  43025  iunconnlem2  45212  islptre  45902  ormkglobd  47156  fcoresf1  47352  2reu8i  47396  lmod1  48775