Theorem ralrimivv 3113

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

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

This theorem is referenced by:  ralrimivva  3114  ralrimdvv  3116  reuind  3683  disjiund  5060  disjxiun  5067  somo  5531  ssrel2  5685  sorpsscmpl  7565  f1o2ndf1  7934  soxp  7941  smoiso  8164  smo11  8166  fiint  9021  sornom  9964  axdc4lem  10142  zorn2lem6  10188  fpwwe2lem11  10328  fpwwe2lem12  10329  nqereu  10616  genpnnp  10692  receu  11550  lbreu  11855  injresinj  13436  sqrmo  14891  iscatd  17299  isfuncd  17496  0subm  18371  insubm  18372  sursubmefmnd  18450  injsubmefmnd  18451  cycsubm  18736  symgextf1  18944  lsmsubm  19173  iscmnd  19314  qusabl  19381  cycsubmcmn  19404  dprdsubg  19542  issrngd  20036  quscrng  20424  mamudm  21447  mat1dimcrng  21534  mavmuldm  21607  fitop  21957  tgcl  22027  topbas  22030  ppttop  22065  epttop  22067  restbas  22217  isnrm2  22417  isnrm3  22418  2ndcctbss  22514  txbas  22626  txbasval  22665  txhaus  22706  xkohaus  22712  basqtop  22770  opnfbas  22901  isfild  22917  filfi  22918  neifil  22939  fbasrn  22943  filufint  22979  rnelfmlem  23011  fmfnfmlem3  23015  fmfnfm  23017  blfps  23467  blf  23468  blbas  23491  minveclem3b  24497  aalioulem2  25398  axcontlem9  27243  upgrwlkdvdelem  28005  grpodivf  28801  ipf  28976  ocsh  29546  adjadj  30199  unopadj2  30201  hmopadj  30202  hmopbdoptHIL  30251  lnopmi  30263  adjlnop  30349  xreceu  31098  esumcocn  31948  bnj1384  32912  f1resrcmplf1d  32959  mclsax  33431  dfon2  33674  nocvxmin  33900  outsideofeu  34360  hilbert1.2  34384  opnrebl2  34437  nn0prpw  34439  fness  34465  tailfb  34493  ontopbas  34544  neificl  35838  metf1o  35840  crngohomfo  36091  smprngopr  36137  ispridlc  36155  prter2  36822  snatpsubN  37691  pclclN  37832  pclfinN  37841  ltrncnv  38087  cdleme24  38293  cdleme28  38314  cdleme50ltrn  38498  cdleme  38501  ltrnco  38660  cdlemk28-3  38849  diaf11N  38990  dibf11N  39102  dihlsscpre  39175  mapdpg  39647  mapdh9a  39730  mapdh9aOLDN  39731  hdmap14lem6  39814  mzpincl  40472  mzpindd  40484  iunconnlem2  42444  islptre  43050  fcoresf1  44450  2reu8i  44492  lmod1  45721