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  5575  ssrel2  5738  sorpsscmpl  7685  resf1extb  7882  f1o2ndf1  8069  soxp  8076  smoiso  8299  smo11  8301  fiint  9234  sornom  10196  axdc4lem  10374  zorn2lem6  10420  fpwwe2lem11  10561  fpwwe2lem12  10562  nqereu  10849  genpnnp  10925  receu  11792  lbreu  12103  injresinj  13743  sqrmo  15210  iscatd  17636  isfuncd  17829  0subm  18782  insubm  18783  sursubmefmnd  18861  injsubmefmnd  18862  cycsubm  19174  symgextf1  19393  lsmsubm  19625  iscmnd  19766  qusabl  19837  cycsubmcmn  19861  dprdsubg  19998  issrngd  20829  quscrng  21278  mamudm  22357  mat1dimcrng  22439  mavmuldm  22512  fitop  22862  tgcl  22931  topbas  22934  ppttop  22969  epttop  22971  restbas  23120  isnrm2  23320  isnrm3  23321  2ndcctbss  23417  txbas  23529  txbasval  23568  txhaus  23609  xkohaus  23615  basqtop  23673  opnfbas  23804  isfild  23820  filfi  23821  neifil  23842  fbasrn  23846  filufint  23882  rnelfmlem  23914  fmfnfmlem3  23918  fmfnfm  23920  blfps  24368  blf  24369  blbas  24392  minveclem3b  25392  aalioulem2  26296  nocvxmin  27744  negsprop  28024  axcontlem9  29038  upgrwlkdvdelem  29801  grpodivf  30606  ipf  30781  ocsh  31351  adjadj  32004  unopadj2  32006  hmopadj  32007  hmopbdoptHIL  32056  lnopmi  32068  adjlnop  32154  xreceu  32978  esumcocn  34221  bnj1384  35171  f1resrcmplf1d  35227  mclsax  35748  dfon2  35969  outsideofeu  36310  hilbert1.2  36334  opnrebl2  36500  nn0prpw  36502  fness  36528  tailfb  36556  ontopbas  36607  neificl  38071  metf1o  38073  crngohomfo  38324  smprngopr  38370  ispridlc  38388  disjdmqsss  39223  disjdmqscossss  39224  eldisjs6  39258  prter2  39324  snatpsubN  40193  pclclN  40334  pclfinN  40343  ltrncnv  40589  cdleme24  40795  cdleme28  40816  cdleme50ltrn  41000  cdleme  41003  ltrnco  41162  cdlemk28-3  41351  diaf11N  41492  dibf11N  41604  dihlsscpre  41677  mapdpg  42149  mapdh9a  42232  mapdh9aOLDN  42233  hdmap14lem6  42316  mzpincl  43163  mzpindd  43175  iunconnlem2  45358  islptre  46046  ormkglobd  47300  fcoresf1  47508  2reu8i  47552  lmod1  48959