Theorem ralrimivv 3197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3061

This theorem is referenced by:  ralrimivva  3199  ralrimdvv  3200  reuind  3749  disjiund  5138  disjxiun  5145  somo  5625  ssrel2  5785  sorpsscmpl  7728  f1o2ndf1  8112  soxp  8119  smoiso  8366  smo11  8368  fiint  9328  sornom  10276  axdc4lem  10454  zorn2lem6  10500  fpwwe2lem11  10640  fpwwe2lem12  10641  nqereu  10928  genpnnp  11004  receu  11864  lbreu  12169  injresinj  13758  sqrmo  15203  iscatd  17622  isfuncd  17820  0subm  18735  insubm  18736  sursubmefmnd  18814  injsubmefmnd  18815  cycsubm  19118  symgextf1  19331  lsmsubm  19563  iscmnd  19704  qusabl  19775  cycsubmcmn  19799  dprdsubg  19936  issrngd  20613  quscrng  21030  mamudm  22111  mat1dimcrng  22200  mavmuldm  22273  fitop  22623  tgcl  22693  topbas  22696  ppttop  22731  epttop  22733  restbas  22883  isnrm2  23083  isnrm3  23084  2ndcctbss  23180  txbas  23292  txbasval  23331  txhaus  23372  xkohaus  23378  basqtop  23436  opnfbas  23567  isfild  23583  filfi  23584  neifil  23605  fbasrn  23609  filufint  23645  rnelfmlem  23677  fmfnfmlem3  23681  fmfnfm  23683  blfps  24133  blf  24134  blbas  24157  minveclem3b  25177  aalioulem2  26083  nocvxmin  27517  negsprop  27749  axcontlem9  28498  upgrwlkdvdelem  29261  grpodivf  30059  ipf  30234  ocsh  30804  adjadj  31457  unopadj2  31459  hmopadj  31460  hmopbdoptHIL  31509  lnopmi  31521  adjlnop  31607  xreceu  32356  esumcocn  33377  bnj1384  34342  f1resrcmplf1d  34389  mclsax  34859  dfon2  35069  outsideofeu  35408  hilbert1.2  35432  opnrebl2  35510  nn0prpw  35512  fness  35538  tailfb  35566  ontopbas  35617  neificl  36925  metf1o  36927  crngohomfo  37178  smprngopr  37224  ispridlc  37242  disjdmqsss  37976  disjdmqscossss  37977  prter2  38055  snatpsubN  38925  pclclN  39066  pclfinN  39075  ltrncnv  39321  cdleme24  39527  cdleme28  39548  cdleme50ltrn  39732  cdleme  39735  ltrnco  39894  cdlemk28-3  40083  diaf11N  40224  dibf11N  40336  dihlsscpre  40409  mapdpg  40881  mapdh9a  40964  mapdh9aOLDN  40965  hdmap14lem6  41048  mzpincl  41775  mzpindd  41787  iunconnlem2  43999  islptre  44634  fcoresf1  46078  2reu8i  46120  lmod1  47261