Theorem ralrimivv 3152

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ral 3095

This theorem is referenced by:  ralrimivva  3153  ralrimdvv  3155  reuind  3628  disjiund  4877  disjxiun  4883  somo  5310  ssrel2  5457  sorpsscmpl  7225  f1o2ndf1  7566  soxp  7571  smoiso  7742  smo11  7744  fiint  8525  sornom  9434  axdc4lem  9612  zorn2lem6  9658  fpwwe2lem12  9798  fpwwe2lem13  9799  nqereu  10086  genpnnp  10162  receu  11020  lbreu  11327  injresinj  12908  sqrmo  14399  iscatd  16719  isfuncd  16910  symgextf1  18224  lsmsubm  18452  iscmnd  18591  qusabl  18654  dprdsubg  18810  issrngd  19253  quscrng  19637  mamudm  20598  mat1dimcrng  20688  mavmuldm  20761  fitop  21112  tgcl  21181  topbas  21184  ppttop  21219  epttop  21221  restbas  21370  isnrm2  21570  isnrm3  21571  2ndcctbss  21667  txbas  21779  txbasval  21818  txhaus  21859  xkohaus  21865  basqtop  21923  opnfbas  22054  isfild  22070  filfi  22071  neifil  22092  fbasrn  22096  filufint  22132  rnelfmlem  22164  fmfnfmlem3  22168  fmfnfm  22170  blfps  22619  blf  22620  blbas  22643  minveclem3b  23634  aalioulem2  24525  axcontlem9  26321  upgrwlkdvdelem  27088  grpodivf  27965  ipf  28140  ocsh  28714  adjadj  29367  unopadj2  29369  hmopadj  29370  hmopbdoptHIL  29419  lnopmi  29431  adjlnop  29517  xreceu  30192  esumcocn  30740  bnj1384  31699  mclsax  32065  dfon2  32285  nocvxmin  32483  outsideofeu  32827  hilbert1.2  32851  opnrebl2  32904  nn0prpw  32906  fness  32932  tailfb  32960  ontopbas  33010  neificl  34173  metf1o  34175  crngohomfo  34429  smprngopr  34475  ispridlc  34493  prter2  35035  snatpsubN  35904  pclclN  36045  pclfinN  36054  ltrncnv  36300  cdleme24  36506  cdleme28  36527  cdleme50ltrn  36711  cdleme  36714  ltrnco  36873  cdlemk28-3  37062  diaf11N  37203  dibf11N  37315  dihlsscpre  37388  mapdpg  37860  mapdh9a  37943  mapdh9aOLDN  37944  hdmap14lem6  38027  mzpincl  38257  mzpindd  38269  iunconnlem2  40104  islptre  40759  2reu8i  42154  lmod1  43296