Theorem ralrimivv 3178

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralrimivva  3180  ralrimdvv  3181  reuind  3724  disjiund  5098  disjxiun  5104  somo  5585  ssrel2  5748  sorpsscmpl  7710  resf1extb  7910  f1o2ndf1  8101  soxp  8108  smoiso  8331  smo11  8333  fiint  9277  fiintOLD  9278  sornom  10230  axdc4lem  10408  zorn2lem6  10454  fpwwe2lem11  10594  fpwwe2lem12  10595  nqereu  10882  genpnnp  10958  receu  11823  lbreu  12133  injresinj  13749  sqrmo  15217  iscatd  17634  isfuncd  17827  0subm  18744  insubm  18745  sursubmefmnd  18823  injsubmefmnd  18824  cycsubm  19134  symgextf1  19351  lsmsubm  19583  iscmnd  19724  qusabl  19795  cycsubmcmn  19819  dprdsubg  19956  issrngd  20764  quscrng  21193  mamudm  22282  mat1dimcrng  22364  mavmuldm  22437  fitop  22787  tgcl  22856  topbas  22859  ppttop  22894  epttop  22896  restbas  23045  isnrm2  23245  isnrm3  23246  2ndcctbss  23342  txbas  23454  txbasval  23493  txhaus  23534  xkohaus  23540  basqtop  23598  opnfbas  23729  isfild  23745  filfi  23746  neifil  23767  fbasrn  23771  filufint  23807  rnelfmlem  23839  fmfnfmlem3  23843  fmfnfm  23845  blfps  24294  blf  24295  blbas  24318  minveclem3b  25328  aalioulem2  26241  nocvxmin  27690  negsprop  27941  axcontlem9  28899  upgrwlkdvdelem  29666  grpodivf  30467  ipf  30642  ocsh  31212  adjadj  31865  unopadj2  31867  hmopadj  31868  hmopbdoptHIL  31917  lnopmi  31929  adjlnop  32015  xreceu  32842  esumcocn  34070  bnj1384  35022  f1resrcmplf1d  35077  mclsax  35556  dfon2  35780  outsideofeu  36119  hilbert1.2  36143  opnrebl2  36309  nn0prpw  36311  fness  36337  tailfb  36365  ontopbas  36416  neificl  37747  metf1o  37749  crngohomfo  38000  smprngopr  38046  ispridlc  38064  disjdmqsss  38794  disjdmqscossss  38795  prter2  38874  snatpsubN  39744  pclclN  39885  pclfinN  39894  ltrncnv  40140  cdleme24  40346  cdleme28  40367  cdleme50ltrn  40551  cdleme  40554  ltrnco  40713  cdlemk28-3  40902  diaf11N  41043  dibf11N  41155  dihlsscpre  41228  mapdpg  41700  mapdh9a  41783  mapdh9aOLDN  41784  hdmap14lem6  41867  mzpincl  42722  mzpindd  42734  iunconnlem2  44924  islptre  45617  ormkglobd  46873  fcoresf1  47070  2reu8i  47114  lmod1  48481