Theorem ralrimivv 3206

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  ralrimivva  3208  ralrimdvv  3209  reuind  3775  disjiund  5157  disjxiun  5163  somo  5646  ssrel2  5809  sorpsscmpl  7769  f1o2ndf1  8163  soxp  8170  smoiso  8418  smo11  8420  fiint  9394  fiintOLD  9395  sornom  10346  axdc4lem  10524  zorn2lem6  10570  fpwwe2lem11  10710  fpwwe2lem12  10711  nqereu  10998  genpnnp  11074  receu  11935  lbreu  12245  injresinj  13838  sqrmo  15300  iscatd  17731  isfuncd  17929  0subm  18852  insubm  18853  sursubmefmnd  18931  injsubmefmnd  18932  cycsubm  19242  symgextf1  19463  lsmsubm  19695  iscmnd  19836  qusabl  19907  cycsubmcmn  19931  dprdsubg  20068  issrngd  20878  quscrng  21316  mamudm  22420  mat1dimcrng  22504  mavmuldm  22577  fitop  22927  tgcl  22997  topbas  23000  ppttop  23035  epttop  23037  restbas  23187  isnrm2  23387  isnrm3  23388  2ndcctbss  23484  txbas  23596  txbasval  23635  txhaus  23676  xkohaus  23682  basqtop  23740  opnfbas  23871  isfild  23887  filfi  23888  neifil  23909  fbasrn  23913  filufint  23949  rnelfmlem  23981  fmfnfmlem3  23985  fmfnfm  23987  blfps  24437  blf  24438  blbas  24461  minveclem3b  25481  aalioulem2  26393  nocvxmin  27841  negsprop  28085  axcontlem9  29005  upgrwlkdvdelem  29772  grpodivf  30570  ipf  30745  ocsh  31315  adjadj  31968  unopadj2  31970  hmopadj  31971  hmopbdoptHIL  32020  lnopmi  32032  adjlnop  32118  xreceu  32886  esumcocn  34044  bnj1384  35008  f1resrcmplf1d  35063  mclsax  35537  dfon2  35756  outsideofeu  36095  hilbert1.2  36119  opnrebl2  36287  nn0prpw  36289  fness  36315  tailfb  36343  ontopbas  36394  neificl  37713  metf1o  37715  crngohomfo  37966  smprngopr  38012  ispridlc  38030  disjdmqsss  38758  disjdmqscossss  38759  prter2  38837  snatpsubN  39707  pclclN  39848  pclfinN  39857  ltrncnv  40103  cdleme24  40309  cdleme28  40330  cdleme50ltrn  40514  cdleme  40517  ltrnco  40676  cdlemk28-3  40865  diaf11N  41006  dibf11N  41118  dihlsscpre  41191  mapdpg  41663  mapdh9a  41746  mapdh9aOLDN  41747  hdmap14lem6  41830  mzpincl  42690  mzpindd  42702  iunconnlem2  44906  islptre  45540  fcoresf1  46984  2reu8i  47028  lmod1  48221