Theorem ralrimivv 3203

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralrimivva  3205  ralrimdvv  3206  reuind  3710  disjiund  5093  disjxiun  5099  somo  5597  ssrel2  5760  f1resrcmplf1d  7279  sorpsscmpl  7750  resf1extb  7946  f1o2ndf1  8133  soxp  8141  smoiso  8370  smo11  8372  fiint  9318  sornom  10355  axdc4lem  10533  zorn2lem6  10579  fpwwe2lem11  10726  fpwwe2lem12  10727  nqereu  11014  genpnnp  11090  receu  11961  lbreu  12267  injresinj  13926  sqrmo  15418  iscatd  17847  isfuncd  18040  0subm  19013  insubm  19014  sursubmefmnd  19092  injsubmefmnd  19093  cycsubm  19417  symgextf1  19635  lsmsubm  19867  iscmnd  20008  qusabl  20079  cycsubmcmn  20103  dprdsubg  20240  crngrhmfo  20726  issrngd  21112  quscrng  21579  mamudm  22710  mat1dimcrng  22792  mavmuldm  22865  fitop  23218  tgcl  23287  topbas  23290  ppttop  23325  epttop  23327  restbas  23476  isnrm2  23676  isnrm3  23677  2ndcctbss  23774  txbas  23886  txbasval  23925  txhaus  23966  xkohaus  23972  basqtop  24030  opnfbas  24161  isfild  24177  filfi  24178  neifil  24199  fbasrn  24203  filufint  24239  rnelfmlem  24271  fmfnfmlem3  24275  fmfnfm  24277  blfps  24725  blf  24726  blbas  24749  minveclem3b  25749  aalioulem2  26660  nocvxmin  28141  negsprop  28421  axcontlem9  29550  upgrwlkdvdelem  30322  grpodivf  31140  ipf  31315  ocsh  31885  adjadj  32538  unopadj2  32540  hmopadj  32541  hmopbdoptHIL  32590  lnopmi  32602  adjlnop  32688  xreceu  33488  esumcocn  34712  bnj1384  35662  mclsax  36334  dfon2  36554  outsideofeu  36896  hilbert1.2  36920  opnrebl2  37109  nn0prpw  37111  fness  37137  tailfb  37165  ontopbas  37216  mh-inf3f1  37329  neificl  38688  metf1o  38690  crngohomfo  38941  smprngopr  38987  ispridlc  39005  disjdmqsss  39838  disjdmqscossss  39839  eldisjs6  39873  prter2  39939  snatpsubN  40808  pclclN  40949  pclfinN  40958  ltrncnv  41204  cdleme24  41410  cdleme28  41431  cdleme50ltrn  41615  cdleme  41618  ltrnco  41777  cdlemk28-3  41966  diaf11N  42107  dibf11N  42219  dihlsscpre  42292  mapdpg  42764  mapdh9a  42847  mapdh9aOLDN  42848  hdmap14lem6  42931  mzpincl  43745  mzpindd  43757  iunconnlem2  45917  islptre  46631  ormkglobd  47887  fcoresf1  48139  2reu8i  48183  smprngprmrng  49436  lmod1  49604