Theorem ralrimivv 3198

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

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

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

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

This theorem is referenced by:  ralrimivva  3200  ralrimdvv  3201  reuind  3749  disjiund  5138  disjxiun  5145  somo  5625  ssrel2  5785  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  11861  lbreu  12166  injresinj  13755  sqrmo  15200  iscatd  17619  isfuncd  17817  0subm  18700  insubm  18701  sursubmefmnd  18779  injsubmefmnd  18780  cycsubm  19081  symgextf1  19291  lsmsubm  19523  iscmnd  19664  qusabl  19735  cycsubmcmn  19759  dprdsubg  19896  issrngd  20473  quscrng  20884  mamudm  21897  mat1dimcrng  21986  mavmuldm  22059  fitop  22409  tgcl  22479  topbas  22482  ppttop  22517  epttop  22519  restbas  22669  isnrm2  22869  isnrm3  22870  2ndcctbss  22966  txbas  23078  txbasval  23117  txhaus  23158  xkohaus  23164  basqtop  23222  opnfbas  23353  isfild  23369  filfi  23370  neifil  23391  fbasrn  23395  filufint  23431  rnelfmlem  23463  fmfnfmlem3  23467  fmfnfm  23469  blfps  23919  blf  23920  blbas  23943  minveclem3b  24952  aalioulem2  25853  nocvxmin  27287  negsprop  27519  axcontlem9  28268  upgrwlkdvdelem  29031  grpodivf  29829  ipf  30004  ocsh  30574  adjadj  31227  unopadj2  31229  hmopadj  31230  hmopbdoptHIL  31279  lnopmi  31291  adjlnop  31377  xreceu  32126  esumcocn  33147  bnj1384  34112  f1resrcmplf1d  34159  mclsax  34629  dfon2  34833  outsideofeu  35172  hilbert1.2  35196  opnrebl2  35292  nn0prpw  35294  fness  35320  tailfb  35348  ontopbas  35399  neificl  36707  metf1o  36709  crngohomfo  36960  smprngopr  37006  ispridlc  37024  disjdmqsss  37758  disjdmqscossss  37759  prter2  37837  snatpsubN  38707  pclclN  38848  pclfinN  38857  ltrncnv  39103  cdleme24  39309  cdleme28  39330  cdleme50ltrn  39514  cdleme  39517  ltrnco  39676  cdlemk28-3  39865  diaf11N  40006  dibf11N  40118  dihlsscpre  40191  mapdpg  40663  mapdh9a  40746  mapdh9aOLDN  40747  hdmap14lem6  40830  mzpincl  41554  mzpindd  41566  iunconnlem2  43778  islptre  44414  fcoresf1  45858  2reu8i  45900  lmod1  47251