Theorem ralrimivv 3207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  ralrimivva  3209  ralrimdvv  3210  reuind  3714  disjiund  5097  disjxiun  5103  somo  5602  ssrel2  5766  f1resrcmplf1d  7299  sorpsscmpl  7771  resf1extb  7967  f1o2ndf1  8157  soxp  8165  smoiso  8395  smo11  8397  fiint  9343  sornom  10379  axdc4lem  10557  zorn2lem6  10603  fpwwe2lem11  10750  fpwwe2lem12  10751  nqereu  11038  genpnnp  11114  receu  11985  lbreu  12291  injresinj  13950  sqrmo  15444  iscatd  17873  isfuncd  18066  0subm  19039  insubm  19040  sursubmefmnd  19118  injsubmefmnd  19119  cycsubm  19443  symgextf1  19662  lsmsubm  19894  iscmnd  20035  qusabl  20106  cycsubmcmn  20130  dprdsubg  20267  crngrhmfo  20753  issrngd  21139  quscrng  21606  mamudm  22737  mat1dimcrng  22819  mavmuldm  22892  fitop  23245  tgcl  23314  topbas  23317  ppttop  23352  epttop  23354  restbas  23503  isnrm2  23703  isnrm3  23704  2ndcctbss  23801  txbas  23913  txbasval  23952  txhaus  23993  xkohaus  23999  basqtop  24057  opnfbas  24188  isfild  24204  filfi  24205  neifil  24226  fbasrn  24230  filufint  24266  rnelfmlem  24298  fmfnfmlem3  24302  fmfnfm  24304  blfps  24752  blf  24753  blbas  24776  minveclem3b  25776  aalioulem2  26687  nocvxmin  28168  negsprop  28448  axcontlem9  29577  upgrwlkdvdelem  30349  grpodivf  31167  ipf  31342  ocsh  31912  adjadj  32565  unopadj2  32567  hmopadj  32568  hmopbdoptHIL  32617  lnopmi  32629  adjlnop  32715  xreceu  33555  esumcocn  34779  bnj1384  35729  mclsax  36500  dfon2  36731  outsideofeu  37073  hilbert1.2  37097  opnrebl2  37286  nn0prpw  37288  fness  37314  tailfb  37342  ontopbas  37393  mh-inf3f1  37506  neificl  38878  metf1o  38880  crngohomfo  39131  smprngopr  39177  ispridlc  39195  disjdmqsss  40028  disjdmqscossss  40029  eldisjs6  40063  prter2  40129  snatpsubN  40998  pclclN  41139  pclfinN  41148  ltrncnv  41394  cdleme24  41600  cdleme28  41621  cdleme50ltrn  41805  cdleme  41808  ltrnco  41967  cdlemk28-3  42156  diaf11N  42297  dibf11N  42409  dihlsscpre  42482  mapdpg  42954  mapdh9a  43037  mapdh9aOLDN  43038  hdmap14lem6  43121  mzpincl  43936  mzpindd  43948  iunconnlem2  46106  islptre  46834  ormkglobd  48090  fcoresf1  48342  2reu8i  48387  smprngprmrng  49639  lmod1  49807