Theorem ralrimivv 3116

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∀wral 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3071

This theorem is referenced by:  ralrimivva  3117  ralrimdvv  3119  reuind  3692  disjiund  5069  disjxiun  5076  somo  5541  ssrel2  5695  sorpsscmpl  7581  f1o2ndf1  7954  soxp  7961  smoiso  8184  smo11  8186  fiint  9069  sornom  10034  axdc4lem  10212  zorn2lem6  10258  fpwwe2lem11  10398  fpwwe2lem12  10399  nqereu  10686  genpnnp  10762  receu  11620  lbreu  11925  injresinj  13506  sqrmo  14961  iscatd  17380  isfuncd  17578  0subm  18454  insubm  18455  sursubmefmnd  18533  injsubmefmnd  18534  cycsubm  18819  symgextf1  19027  lsmsubm  19256  iscmnd  19397  qusabl  19464  cycsubmcmn  19487  dprdsubg  19625  issrngd  20119  quscrng  20509  mamudm  21535  mat1dimcrng  21624  mavmuldm  21697  fitop  22047  tgcl  22117  topbas  22120  ppttop  22155  epttop  22157  restbas  22307  isnrm2  22507  isnrm3  22508  2ndcctbss  22604  txbas  22716  txbasval  22755  txhaus  22796  xkohaus  22802  basqtop  22860  opnfbas  22991  isfild  23007  filfi  23008  neifil  23029  fbasrn  23033  filufint  23069  rnelfmlem  23101  fmfnfmlem3  23105  fmfnfm  23107  blfps  23557  blf  23558  blbas  23581  minveclem3b  24590  aalioulem2  25491  axcontlem9  27338  upgrwlkdvdelem  28100  grpodivf  28896  ipf  29071  ocsh  29641  adjadj  30294  unopadj2  30296  hmopadj  30297  hmopbdoptHIL  30346  lnopmi  30358  adjlnop  30444  xreceu  31192  esumcocn  32044  bnj1384  33008  f1resrcmplf1d  33055  mclsax  33527  dfon2  33764  nocvxmin  33969  outsideofeu  34429  hilbert1.2  34453  opnrebl2  34506  nn0prpw  34508  fness  34534  tailfb  34562  ontopbas  34613  neificl  35907  metf1o  35909  crngohomfo  36160  smprngopr  36206  ispridlc  36224  prter2  36891  snatpsubN  37760  pclclN  37901  pclfinN  37910  ltrncnv  38156  cdleme24  38362  cdleme28  38383  cdleme50ltrn  38567  cdleme  38570  ltrnco  38729  cdlemk28-3  38918  diaf11N  39059  dibf11N  39171  dihlsscpre  39244  mapdpg  39716  mapdh9a  39799  mapdh9aOLDN  39800  hdmap14lem6  39883  mzpincl  40553  mzpindd  40565  iunconnlem2  42525  islptre  43131  fcoresf1  44531  2reu8i  44573  lmod1  45802