Theorem ralrimivv 3197

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  ralrimivva  3199  ralrimdvv  3200  reuind  3761  disjiund  5138  disjxiun  5144  somo  5634  ssrel2  5797  sorpsscmpl  7752  f1o2ndf1  8145  soxp  8152  smoiso  8400  smo11  8402  fiint  9363  fiintOLD  9364  sornom  10314  axdc4lem  10492  zorn2lem6  10538  fpwwe2lem11  10678  fpwwe2lem12  10679  nqereu  10966  genpnnp  11042  receu  11905  lbreu  12215  injresinj  13823  sqrmo  15286  iscatd  17717  isfuncd  17915  0subm  18842  insubm  18843  sursubmefmnd  18921  injsubmefmnd  18922  cycsubm  19232  symgextf1  19453  lsmsubm  19685  iscmnd  19826  qusabl  19897  cycsubmcmn  19921  dprdsubg  20058  issrngd  20872  quscrng  21310  mamudm  22414  mat1dimcrng  22498  mavmuldm  22571  fitop  22921  tgcl  22991  topbas  22994  ppttop  23029  epttop  23031  restbas  23181  isnrm2  23381  isnrm3  23382  2ndcctbss  23478  txbas  23590  txbasval  23629  txhaus  23670  xkohaus  23676  basqtop  23734  opnfbas  23865  isfild  23881  filfi  23882  neifil  23903  fbasrn  23907  filufint  23943  rnelfmlem  23975  fmfnfmlem3  23979  fmfnfm  23981  blfps  24431  blf  24432  blbas  24455  minveclem3b  25475  aalioulem2  26389  nocvxmin  27837  negsprop  28081  axcontlem9  29001  upgrwlkdvdelem  29768  grpodivf  30566  ipf  30741  ocsh  31311  adjadj  31964  unopadj2  31966  hmopadj  31967  hmopbdoptHIL  32016  lnopmi  32028  adjlnop  32114  xreceu  32888  esumcocn  34060  bnj1384  35024  f1resrcmplf1d  35079  mclsax  35553  dfon2  35773  outsideofeu  36112  hilbert1.2  36136  opnrebl2  36303  nn0prpw  36305  fness  36331  tailfb  36359  ontopbas  36410  neificl  37739  metf1o  37741  crngohomfo  37992  smprngopr  38038  ispridlc  38056  disjdmqsss  38783  disjdmqscossss  38784  prter2  38862  snatpsubN  39732  pclclN  39873  pclfinN  39882  ltrncnv  40128  cdleme24  40334  cdleme28  40355  cdleme50ltrn  40539  cdleme  40542  ltrnco  40701  cdlemk28-3  40890  diaf11N  41031  dibf11N  41143  dihlsscpre  41216  mapdpg  41688  mapdh9a  41771  mapdh9aOLDN  41772  hdmap14lem6  41855  mzpincl  42721  mzpindd  42733  iunconnlem2  44932  islptre  45574  fcoresf1  47018  2reu8i  47062  lmod1  48337