Theorem ralrimivv 3203

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

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

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 1943

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

This theorem is used by:  ralrimivva  3205  ralrimdvv  3206  reuind  3711  disjiund  5094  disjxiun  5100  somo  5602  ssrel2  5765  f1resrcmplf1d  7272  sorpsscmpl  7735  resf1extb  7931  f1o2ndf1  8119  soxp  8127  smoiso  8351  smo11  8353  fiint  9296  sornom  10279  axdc4lem  10457  zorn2lem6  10503  fpwwe2lem11  10650  fpwwe2lem12  10651  nqereu  10938  genpnnp  11014  receu  11883  lbreu  12189  injresinj  13847  sqrmo  15338  iscatd  17761  isfuncd  17954  0subm  18926  insubm  18927  sursubmefmnd  19005  injsubmefmnd  19006  cycsubm  19330  symgextf1  19548  lsmsubm  19780  iscmnd  19921  qusabl  19992  cycsubmcmn  20016  dprdsubg  20153  crngrhmfo  20637  issrngd  21021  quscrng  21486  mamudm  22617  mat1dimcrng  22699  mavmuldm  22772  fitop  23125  tgcl  23194  topbas  23197  ppttop  23232  epttop  23234  restbas  23383  isnrm2  23583  isnrm3  23584  2ndcctbss  23681  txbas  23793  txbasval  23832  txhaus  23873  xkohaus  23879  basqtop  23937  opnfbas  24068  isfild  24084  filfi  24085  neifil  24106  fbasrn  24110  filufint  24146  rnelfmlem  24178  fmfnfmlem3  24182  fmfnfm  24184  blfps  24632  blf  24633  blbas  24656  minveclem3b  25656  aalioulem2  26569  nocvxmin  28020  negsprop  28300  axcontlem9  29429  upgrwlkdvdelem  30201  grpodivf  31019  ipf  31194  ocsh  31764  adjadj  32417  unopadj2  32419  hmopadj  32420  hmopbdoptHIL  32469  lnopmi  32481  adjlnop  32567  xreceu  33367  esumcocn  34590  bnj1384  35541  mclsax  36148  dfon2  36369  outsideofeu  36711  hilbert1.2  36735  opnrebl2  36940  nn0prpw  36942  fness  36968  tailfb  36996  ontopbas  37047  neificl  38503  metf1o  38505  crngohomfo  38756  smprngopr  38802  ispridlc  38820  disjdmqsss  39653  disjdmqscossss  39654  eldisjs6  39688  prter2  39754  snatpsubN  40623  pclclN  40764  pclfinN  40773  ltrncnv  41019  cdleme24  41225  cdleme28  41246  cdleme50ltrn  41430  cdleme  41433  ltrnco  41592  cdlemk28-3  41781  diaf11N  41922  dibf11N  42034  dihlsscpre  42107  mapdpg  42579  mapdh9a  42662  mapdh9aOLDN  42663  hdmap14lem6  42746  mzpincl  43579  mzpindd  43591  iunconnlem2  45757  islptre  46449  ormkglobd  47705  fcoresf1  47957  2reu8i  48001  smprngprmrng  49254  lmod1  49422