Theorem ralrimivv 3170

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 3127	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜓))
4	3	ralrimiv 3120	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  3172  ralrimdvv  3173  reuind  3713  disjiund  5083  disjxiun  5089  somo  5566  ssrel2  5728  sorpsscmpl  7670  resf1extb  7867  f1o2ndf1  8055  soxp  8062  smoiso  8285  smo11  8287  fiint  9216  fiintOLD  9217  sornom  10171  axdc4lem  10349  zorn2lem6  10395  fpwwe2lem11  10535  fpwwe2lem12  10536  nqereu  10823  genpnnp  10899  receu  11765  lbreu  12075  injresinj  13691  sqrmo  15158  iscatd  17579  isfuncd  17772  0subm  18691  insubm  18692  sursubmefmnd  18770  injsubmefmnd  18771  cycsubm  19081  symgextf1  19300  lsmsubm  19532  iscmnd  19673  qusabl  19744  cycsubmcmn  19768  dprdsubg  19905  issrngd  20740  quscrng  21190  mamudm  22280  mat1dimcrng  22362  mavmuldm  22435  fitop  22785  tgcl  22854  topbas  22857  ppttop  22892  epttop  22894  restbas  23043  isnrm2  23243  isnrm3  23244  2ndcctbss  23340  txbas  23452  txbasval  23491  txhaus  23532  xkohaus  23538  basqtop  23596  opnfbas  23727  isfild  23743  filfi  23744  neifil  23765  fbasrn  23769  filufint  23805  rnelfmlem  23837  fmfnfmlem3  23841  fmfnfm  23843  blfps  24292  blf  24293  blbas  24316  minveclem3b  25326  aalioulem2  26239  nocvxmin  27689  negsprop  27948  axcontlem9  28921  upgrwlkdvdelem  29685  grpodivf  30486  ipf  30661  ocsh  31231  adjadj  31884  unopadj2  31886  hmopadj  31887  hmopbdoptHIL  31936  lnopmi  31948  adjlnop  32034  xreceu  32871  esumcocn  34063  bnj1384  35015  f1resrcmplf1d  35070  mclsax  35562  dfon2  35786  outsideofeu  36125  hilbert1.2  36149  opnrebl2  36315  nn0prpw  36317  fness  36343  tailfb  36371  ontopbas  36422  neificl  37753  metf1o  37755  crngohomfo  38006  smprngopr  38052  ispridlc  38070  disjdmqsss  38800  disjdmqscossss  38801  prter2  38880  snatpsubN  39749  pclclN  39890  pclfinN  39899  ltrncnv  40145  cdleme24  40351  cdleme28  40372  cdleme50ltrn  40556  cdleme  40559  ltrnco  40718  cdlemk28-3  40907  diaf11N  41048  dibf11N  41160  dihlsscpre  41233  mapdpg  41705  mapdh9a  41788  mapdh9aOLDN  41789  hdmap14lem6  41872  mzpincl  42727  mzpindd  42739  iunconnlem2  44928  islptre  45620  ormkglobd  46876  fcoresf1  47073  2reu8i  47117  lmod1  48497