Theorem ralrimivv 3122

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  ralrimivva  3123  ralrimdvv  3124  reuind  3688  disjiund  5064  disjxiun  5071  somo  5540  ssrel2  5696  sorpsscmpl  7587  f1o2ndf1  7963  soxp  7970  smoiso  8193  smo11  8195  fiint  9091  sornom  10033  axdc4lem  10211  zorn2lem6  10257  fpwwe2lem11  10397  fpwwe2lem12  10398  nqereu  10685  genpnnp  10761  receu  11620  lbreu  11925  injresinj  13508  sqrmo  14963  iscatd  17382  isfuncd  17580  0subm  18456  insubm  18457  sursubmefmnd  18535  injsubmefmnd  18536  cycsubm  18821  symgextf1  19029  lsmsubm  19258  iscmnd  19399  qusabl  19466  cycsubmcmn  19489  dprdsubg  19627  issrngd  20121  quscrng  20511  mamudm  21537  mat1dimcrng  21626  mavmuldm  21699  fitop  22049  tgcl  22119  topbas  22122  ppttop  22157  epttop  22159  restbas  22309  isnrm2  22509  isnrm3  22510  2ndcctbss  22606  txbas  22718  txbasval  22757  txhaus  22798  xkohaus  22804  basqtop  22862  opnfbas  22993  isfild  23009  filfi  23010  neifil  23031  fbasrn  23035  filufint  23071  rnelfmlem  23103  fmfnfmlem3  23107  fmfnfm  23109  blfps  23559  blf  23560  blbas  23583  minveclem3b  24592  aalioulem2  25493  axcontlem9  27340  upgrwlkdvdelem  28104  grpodivf  28900  ipf  29075  ocsh  29645  adjadj  30298  unopadj2  30300  hmopadj  30301  hmopbdoptHIL  30350  lnopmi  30362  adjlnop  30448  xreceu  31196  esumcocn  32048  bnj1384  33012  f1resrcmplf1d  33059  mclsax  33531  dfon2  33768  nocvxmin  33973  outsideofeu  34433  hilbert1.2  34457  opnrebl2  34510  nn0prpw  34512  fness  34538  tailfb  34566  ontopbas  34617  neificl  35911  metf1o  35913  crngohomfo  36164  smprngopr  36210  ispridlc  36228  prter2  36895  snatpsubN  37764  pclclN  37905  pclfinN  37914  ltrncnv  38160  cdleme24  38366  cdleme28  38387  cdleme50ltrn  38571  cdleme  38574  ltrnco  38733  cdlemk28-3  38922  diaf11N  39063  dibf11N  39175  dihlsscpre  39248  mapdpg  39720  mapdh9a  39803  mapdh9aOLDN  39804  hdmap14lem6  39887  mzpincl  40556  mzpindd  40568  iunconnlem2  42555  islptre  43160  fcoresf1  44563  2reu8i  44605  lmod1  45833