Theorem ralrimivv 3186

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

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

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 3053

This theorem is referenced by:  ralrimivva  3188  ralrimdvv  3189  reuind  3741  disjiund  5115  disjxiun  5121  somo  5605  ssrel2  5769  sorpsscmpl  7733  resf1extb  7935  f1o2ndf1  8126  soxp  8133  smoiso  8381  smo11  8383  fiint  9343  fiintOLD  9344  sornom  10296  axdc4lem  10474  zorn2lem6  10520  fpwwe2lem11  10660  fpwwe2lem12  10661  nqereu  10948  genpnnp  11024  receu  11887  lbreu  12197  injresinj  13809  sqrmo  15275  iscatd  17690  isfuncd  17883  0subm  18800  insubm  18801  sursubmefmnd  18879  injsubmefmnd  18880  cycsubm  19190  symgextf1  19407  lsmsubm  19639  iscmnd  19780  qusabl  19851  cycsubmcmn  19875  dprdsubg  20012  issrngd  20820  quscrng  21249  mamudm  22338  mat1dimcrng  22420  mavmuldm  22493  fitop  22843  tgcl  22912  topbas  22915  ppttop  22950  epttop  22952  restbas  23101  isnrm2  23301  isnrm3  23302  2ndcctbss  23398  txbas  23510  txbasval  23549  txhaus  23590  xkohaus  23596  basqtop  23654  opnfbas  23785  isfild  23801  filfi  23802  neifil  23823  fbasrn  23827  filufint  23863  rnelfmlem  23895  fmfnfmlem3  23899  fmfnfm  23901  blfps  24350  blf  24351  blbas  24374  minveclem3b  25385  aalioulem2  26298  nocvxmin  27747  negsprop  27998  axcontlem9  28956  upgrwlkdvdelem  29723  grpodivf  30524  ipf  30699  ocsh  31269  adjadj  31922  unopadj2  31924  hmopadj  31925  hmopbdoptHIL  31974  lnopmi  31986  adjlnop  32072  xreceu  32901  esumcocn  34116  bnj1384  35068  f1resrcmplf1d  35123  mclsax  35596  dfon2  35815  outsideofeu  36154  hilbert1.2  36178  opnrebl2  36344  nn0prpw  36346  fness  36372  tailfb  36400  ontopbas  36451  neificl  37782  metf1o  37784  crngohomfo  38035  smprngopr  38081  ispridlc  38099  disjdmqsss  38825  disjdmqscossss  38826  prter2  38904  snatpsubN  39774  pclclN  39915  pclfinN  39924  ltrncnv  40170  cdleme24  40376  cdleme28  40397  cdleme50ltrn  40581  cdleme  40584  ltrnco  40743  cdlemk28-3  40932  diaf11N  41073  dibf11N  41185  dihlsscpre  41258  mapdpg  41730  mapdh9a  41813  mapdh9aOLDN  41814  hdmap14lem6  41897  mzpincl  42732  mzpindd  42744  iunconnlem2  44934  islptre  45628  ormkglobd  46884  fcoresf1  47078  2reu8i  47122  lmod1  48448