Theorem ralrimivv 3179

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  ralrimivva  3181  ralrimdvv  3182  reuind  3700  disjiund  5077  disjxiun  5083  somo  5573  ssrel2  5736  sorpsscmpl  7683  resf1extb  7880  f1o2ndf1  8067  soxp  8074  smoiso  8297  smo11  8299  fiint  9232  sornom  10194  axdc4lem  10372  zorn2lem6  10418  fpwwe2lem11  10559  fpwwe2lem12  10560  nqereu  10847  genpnnp  10923  receu  11790  lbreu  12101  injresinj  13741  sqrmo  15208  iscatd  17634  isfuncd  17827  0subm  18780  insubm  18781  sursubmefmnd  18859  injsubmefmnd  18860  cycsubm  19172  symgextf1  19391  lsmsubm  19623  iscmnd  19764  qusabl  19835  cycsubmcmn  19859  dprdsubg  19996  issrngd  20827  quscrng  21277  mamudm  22374  mat1dimcrng  22456  mavmuldm  22529  fitop  22879  tgcl  22948  topbas  22951  ppttop  22986  epttop  22988  restbas  23137  isnrm2  23337  isnrm3  23338  2ndcctbss  23434  txbas  23546  txbasval  23585  txhaus  23626  xkohaus  23632  basqtop  23690  opnfbas  23821  isfild  23837  filfi  23838  neifil  23859  fbasrn  23863  filufint  23899  rnelfmlem  23931  fmfnfmlem3  23935  fmfnfm  23937  blfps  24385  blf  24386  blbas  24409  minveclem3b  25409  aalioulem2  26314  nocvxmin  27765  negsprop  28045  axcontlem9  29059  upgrwlkdvdelem  29823  grpodivf  30628  ipf  30803  ocsh  31373  adjadj  32026  unopadj2  32028  hmopadj  32029  hmopbdoptHIL  32078  lnopmi  32090  adjlnop  32176  xreceu  33000  esumcocn  34244  bnj1384  35194  f1resrcmplf1d  35250  mclsax  35771  dfon2  35992  outsideofeu  36333  hilbert1.2  36357  opnrebl2  36523  nn0prpw  36525  fness  36551  tailfb  36579  ontopbas  36630  neificl  38094  metf1o  38096  crngohomfo  38347  smprngopr  38393  ispridlc  38411  disjdmqsss  39246  disjdmqscossss  39247  eldisjs6  39281  prter2  39347  snatpsubN  40216  pclclN  40357  pclfinN  40366  ltrncnv  40612  cdleme24  40818  cdleme28  40839  cdleme50ltrn  41023  cdleme  41026  ltrnco  41185  cdlemk28-3  41374  diaf11N  41515  dibf11N  41627  dihlsscpre  41700  mapdpg  42172  mapdh9a  42255  mapdh9aOLDN  42256  hdmap14lem6  42339  mzpincl  43186  mzpindd  43198  iunconnlem2  45385  islptre  46073  ormkglobd  47327  fcoresf1  47535  2reu8i  47579  lmod1  48986