Theorem ralrimivv 3196

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  ralrimivva  3198  ralrimdvv  3199  reuind  3748  disjiund  5137  disjxiun  5144  somo  5624  ssrel2  5784  sorpsscmpl  7726  f1o2ndf1  8110  soxp  8117  smoiso  8364  smo11  8366  fiint  9326  sornom  10274  axdc4lem  10452  zorn2lem6  10498  fpwwe2lem11  10638  fpwwe2lem12  10639  nqereu  10926  genpnnp  11002  receu  11863  lbreu  12168  injresinj  13757  sqrmo  15202  iscatd  17621  isfuncd  17819  0subm  18734  insubm  18735  sursubmefmnd  18813  injsubmefmnd  18814  cycsubm  19117  symgextf1  19330  lsmsubm  19562  iscmnd  19703  qusabl  19774  cycsubmcmn  19798  dprdsubg  19935  issrngd  20612  quscrng  21029  mamudm  22110  mat1dimcrng  22199  mavmuldm  22272  fitop  22622  tgcl  22692  topbas  22695  ppttop  22730  epttop  22732  restbas  22882  isnrm2  23082  isnrm3  23083  2ndcctbss  23179  txbas  23291  txbasval  23330  txhaus  23371  xkohaus  23377  basqtop  23435  opnfbas  23566  isfild  23582  filfi  23583  neifil  23604  fbasrn  23608  filufint  23644  rnelfmlem  23676  fmfnfmlem3  23680  fmfnfm  23682  blfps  24132  blf  24133  blbas  24156  minveclem3b  25176  aalioulem2  26082  nocvxmin  27516  negsprop  27748  axcontlem9  28497  upgrwlkdvdelem  29260  grpodivf  30058  ipf  30233  ocsh  30803  adjadj  31456  unopadj2  31458  hmopadj  31459  hmopbdoptHIL  31508  lnopmi  31520  adjlnop  31606  xreceu  32355  esumcocn  33376  bnj1384  34341  f1resrcmplf1d  34388  mclsax  34858  dfon2  35068  outsideofeu  35407  hilbert1.2  35431  opnrebl2  35509  nn0prpw  35511  fness  35537  tailfb  35565  ontopbas  35616  neificl  36924  metf1o  36926  crngohomfo  37177  smprngopr  37223  ispridlc  37241  disjdmqsss  37975  disjdmqscossss  37976  prter2  38054  snatpsubN  38924  pclclN  39065  pclfinN  39074  ltrncnv  39320  cdleme24  39526  cdleme28  39547  cdleme50ltrn  39731  cdleme  39734  ltrnco  39893  cdlemk28-3  40082  diaf11N  40223  dibf11N  40335  dihlsscpre  40408  mapdpg  40880  mapdh9a  40963  mapdh9aOLDN  40964  hdmap14lem6  41047  mzpincl  41774  mzpindd  41786  iunconnlem2  43998  islptre  44633  fcoresf1  46077  2reu8i  46119  lmod1  47260