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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimivva  3178  ralrimdvv  3179  reuind  3721  disjiund  5093  disjxiun  5099  somo  5578  ssrel2  5739  sorpsscmpl  7690  resf1extb  7890  f1o2ndf1  8078  soxp  8085  smoiso  8308  smo11  8310  fiint  9253  fiintOLD  9254  sornom  10208  axdc4lem  10386  zorn2lem6  10432  fpwwe2lem11  10572  fpwwe2lem12  10573  nqereu  10860  genpnnp  10936  receu  11801  lbreu  12111  injresinj  13727  sqrmo  15194  iscatd  17615  isfuncd  17808  0subm  18727  insubm  18728  sursubmefmnd  18806  injsubmefmnd  18807  cycsubm  19117  symgextf1  19336  lsmsubm  19568  iscmnd  19709  qusabl  19780  cycsubmcmn  19804  dprdsubg  19941  issrngd  20776  quscrng  21226  mamudm  22316  mat1dimcrng  22398  mavmuldm  22471  fitop  22821  tgcl  22890  topbas  22893  ppttop  22928  epttop  22930  restbas  23079  isnrm2  23279  isnrm3  23280  2ndcctbss  23376  txbas  23488  txbasval  23527  txhaus  23568  xkohaus  23574  basqtop  23632  opnfbas  23763  isfild  23779  filfi  23780  neifil  23801  fbasrn  23805  filufint  23841  rnelfmlem  23873  fmfnfmlem3  23877  fmfnfm  23879  blfps  24328  blf  24329  blbas  24352  minveclem3b  25362  aalioulem2  26275  nocvxmin  27725  negsprop  27982  axcontlem9  28953  upgrwlkdvdelem  29717  grpodivf  30518  ipf  30693  ocsh  31263  adjadj  31916  unopadj2  31918  hmopadj  31919  hmopbdoptHIL  31968  lnopmi  31980  adjlnop  32066  xreceu  32893  esumcocn  34064  bnj1384  35016  f1resrcmplf1d  35071  mclsax  35550  dfon2  35774  outsideofeu  36113  hilbert1.2  36137  opnrebl2  36303  nn0prpw  36305  fness  36331  tailfb  36359  ontopbas  36410  neificl  37741  metf1o  37743  crngohomfo  37994  smprngopr  38040  ispridlc  38058  disjdmqsss  38788  disjdmqscossss  38789  prter2  38868  snatpsubN  39738  pclclN  39879  pclfinN  39888  ltrncnv  40134  cdleme24  40340  cdleme28  40361  cdleme50ltrn  40545  cdleme  40548  ltrnco  40707  cdlemk28-3  40896  diaf11N  41037  dibf11N  41149  dihlsscpre  41222  mapdpg  41694  mapdh9a  41777  mapdh9aOLDN  41778  hdmap14lem6  41861  mzpincl  42716  mzpindd  42728  iunconnlem2  44918  islptre  45611  ormkglobd  46867  fcoresf1  47064  2reu8i  47108  lmod1  48475