Theorem ralrimivv 3205

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  ralrimivva  3207  ralrimdvv  3208  reuind  3715  disjiund  5099  disjxiun  5105  somo  5607  ssrel2  5770  sorpsscmpl  7733  resf1extb  7929  f1o2ndf1  8115  soxp  8123  smoiso  8347  smo11  8349  fiint  9284  sornom  10267  axdc4lem  10445  zorn2lem6  10491  fpwwe2lem11  10632  fpwwe2lem12  10633  nqereu  10920  genpnnp  10996  receu  11865  lbreu  12171  injresinj  13827  sqrmo  15309  iscatd  17735  isfuncd  17928  0subm  18882  insubm  18883  sursubmefmnd  18961  injsubmefmnd  18962  cycsubm  19279  symgextf1  19497  lsmsubm  19729  iscmnd  19870  qusabl  19941  cycsubmcmn  19965  dprdsubg  20102  crngrhmfo  20585  issrngd  20969  quscrng  21434  mamudm  22563  mat1dimcrng  22645  mavmuldm  22718  fitop  23068  tgcl  23137  topbas  23140  ppttop  23175  epttop  23177  restbas  23326  isnrm2  23526  isnrm3  23527  2ndcctbss  23623  txbas  23735  txbasval  23774  txhaus  23815  xkohaus  23821  basqtop  23879  opnfbas  24010  isfild  24026  filfi  24027  neifil  24048  fbasrn  24052  filufint  24088  rnelfmlem  24120  fmfnfmlem3  24124  fmfnfm  24126  blfps  24574  blf  24575  blbas  24598  minveclem3b  25598  aalioulem2  26507  nocvxmin  27959  negsprop  28239  axcontlem9  29333  upgrwlkdvdelem  30096  grpodivf  30901  ipf  31076  ocsh  31646  adjadj  32299  unopadj2  32301  hmopadj  32302  hmopbdoptHIL  32351  lnopmi  32363  adjlnop  32449  xreceu  33252  esumcocn  34479  bnj1384  35429  f1resrcmplf1d  35484  mclsax  36069  dfon2  36290  outsideofeu  36631  hilbert1.2  36655  opnrebl2  36860  nn0prpw  36862  fness  36888  tailfb  36916  ontopbas  36967  neificl  38432  metf1o  38434  crngohomfo  38685  smprngopr  38731  ispridlc  38749  disjdmqsss  39582  disjdmqscossss  39583  eldisjs6  39617  prter2  39683  snatpsubN  40552  pclclN  40693  pclfinN  40702  ltrncnv  40948  cdleme24  41154  cdleme28  41175  cdleme50ltrn  41359  cdleme  41362  ltrnco  41521  cdlemk28-3  41710  diaf11N  41851  dibf11N  41963  dihlsscpre  42036  mapdpg  42508  mapdh9a  42591  mapdh9aOLDN  42592  hdmap14lem6  42675  mzpincl  43493  mzpindd  43505  iunconnlem2  45671  islptre  46363  ormkglobd  47619  fcoresf1  47834  2reu8i  47878  smprngprmrng  49132  lmod1  49300