Theorem ralrimivv 3176

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

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

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 3045

This theorem is referenced by:  ralrimivva  3178  ralrimdvv  3179  reuind  3721  disjiund  5093  disjxiun  5099  somo  5578  ssrel2  5739  sorpsscmpl  7690  resf1extb  7890  f1o2ndf1  8078  soxp  8085  smoiso  8308  smo11  8310  fiint  9253  fiintOLD  9254  sornom  10206  axdc4lem  10384  zorn2lem6  10430  fpwwe2lem11  10570  fpwwe2lem12  10571  nqereu  10858  genpnnp  10934  receu  11799  lbreu  12109  injresinj  13725  sqrmo  15193  iscatd  17614  isfuncd  17807  0subm  18726  insubm  18727  sursubmefmnd  18805  injsubmefmnd  18806  cycsubm  19116  symgextf1  19335  lsmsubm  19567  iscmnd  19708  qusabl  19779  cycsubmcmn  19803  dprdsubg  19940  issrngd  20775  quscrng  21225  mamudm  22315  mat1dimcrng  22397  mavmuldm  22470  fitop  22820  tgcl  22889  topbas  22892  ppttop  22927  epttop  22929  restbas  23078  isnrm2  23278  isnrm3  23279  2ndcctbss  23375  txbas  23487  txbasval  23526  txhaus  23567  xkohaus  23573  basqtop  23631  opnfbas  23762  isfild  23778  filfi  23779  neifil  23800  fbasrn  23804  filufint  23840  rnelfmlem  23872  fmfnfmlem3  23876  fmfnfm  23878  blfps  24327  blf  24328  blbas  24351  minveclem3b  25361  aalioulem2  26274  nocvxmin  27724  negsprop  27981  axcontlem9  28952  upgrwlkdvdelem  29716  grpodivf  30517  ipf  30692  ocsh  31262  adjadj  31915  unopadj2  31917  hmopadj  31918  hmopbdoptHIL  31967  lnopmi  31979  adjlnop  32065  xreceu  32892  esumcocn  34063  bnj1384  35015  f1resrcmplf1d  35070  mclsax  35549  dfon2  35773  outsideofeu  36112  hilbert1.2  36136  opnrebl2  36302  nn0prpw  36304  fness  36330  tailfb  36358  ontopbas  36409  neificl  37740  metf1o  37742  crngohomfo  37993  smprngopr  38039  ispridlc  38057  disjdmqsss  38787  disjdmqscossss  38788  prter2  38867  snatpsubN  39737  pclclN  39878  pclfinN  39887  ltrncnv  40133  cdleme24  40339  cdleme28  40360  cdleme50ltrn  40544  cdleme  40547  ltrnco  40706  cdlemk28-3  40895  diaf11N  41036  dibf11N  41148  dihlsscpre  41221  mapdpg  41693  mapdh9a  41776  mapdh9aOLDN  41777  hdmap14lem6  41860  mzpincl  42715  mzpindd  42727  iunconnlem2  44917  islptre  45610  ormkglobd  46866  fcoresf1  47063  2reu8i  47107  lmod1  48474