Theorem ralrimivv 3179

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

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

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 3053

This theorem is referenced by:  ralrimivva  3181  ralrimdvv  3182  reuind  3713  disjiund  5091  disjxiun  5097  somo  5581  ssrel2  5744  sorpsscmpl  7691  resf1extb  7888  f1o2ndf1  8076  soxp  8083  smoiso  8306  smo11  8308  fiint  9241  sornom  10201  axdc4lem  10379  zorn2lem6  10425  fpwwe2lem11  10566  fpwwe2lem12  10567  nqereu  10854  genpnnp  10930  receu  11796  lbreu  12106  injresinj  13721  sqrmo  15188  iscatd  17610  isfuncd  17803  0subm  18756  insubm  18757  sursubmefmnd  18835  injsubmefmnd  18836  cycsubm  19148  symgextf1  19367  lsmsubm  19599  iscmnd  19740  qusabl  19811  cycsubmcmn  19835  dprdsubg  19972  issrngd  20805  quscrng  21255  mamudm  22356  mat1dimcrng  22438  mavmuldm  22511  fitop  22861  tgcl  22930  topbas  22933  ppttop  22968  epttop  22970  restbas  23119  isnrm2  23319  isnrm3  23320  2ndcctbss  23416  txbas  23528  txbasval  23567  txhaus  23608  xkohaus  23614  basqtop  23672  opnfbas  23803  isfild  23819  filfi  23820  neifil  23841  fbasrn  23845  filufint  23881  rnelfmlem  23913  fmfnfmlem3  23917  fmfnfm  23919  blfps  24367  blf  24368  blbas  24391  minveclem3b  25401  aalioulem2  26314  nocvxmin  27768  negsprop  28048  axcontlem9  29063  upgrwlkdvdelem  29827  grpodivf  30632  ipf  30807  ocsh  31377  adjadj  32030  unopadj2  32032  hmopadj  32033  hmopbdoptHIL  32082  lnopmi  32094  adjlnop  32180  xreceu  33020  esumcocn  34264  bnj1384  35214  f1resrcmplf1d  35270  mclsax  35791  dfon2  36012  outsideofeu  36353  hilbert1.2  36377  opnrebl2  36543  nn0prpw  36545  fness  36571  tailfb  36599  ontopbas  36650  neificl  38033  metf1o  38035  crngohomfo  38286  smprngopr  38332  ispridlc  38350  disjdmqsss  39185  disjdmqscossss  39186  eldisjs6  39220  prter2  39286  snatpsubN  40155  pclclN  40296  pclfinN  40305  ltrncnv  40551  cdleme24  40757  cdleme28  40778  cdleme50ltrn  40962  cdleme  40965  ltrnco  41124  cdlemk28-3  41313  diaf11N  41454  dibf11N  41566  dihlsscpre  41639  mapdpg  42111  mapdh9a  42194  mapdh9aOLDN  42195  hdmap14lem6  42278  mzpincl  43120  mzpindd  43132  iunconnlem2  45319  islptre  46008  ormkglobd  47262  fcoresf1  47458  2reu8i  47502  lmod1  48881