Theorem ralrimivv 3182

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  ralrimivva  3184  ralrimdvv  3185  reuind  3695  disjiund  5065  disjxiun  5071  somo  5567  ssrel2  5730  sorpsscmpl  7680  resf1extb  7878  f1o2ndf1  8063  soxp  8071  smoiso  8295  smo11  8297  fiint  9231  sornom  10195  axdc4lem  10373  zorn2lem6  10419  fpwwe2lem11  10560  fpwwe2lem12  10561  nqereu  10848  genpnnp  10924  receu  11791  lbreu  12101  injresinj  13741  sqrmo  15208  iscatd  17634  isfuncd  17827  0subm  18780  insubm  18781  sursubmefmnd  18859  injsubmefmnd  18860  cycsubm  19172  symgextf1  19390  lsmsubm  19622  iscmnd  19763  qusabl  19834  cycsubmcmn  19858  dprdsubg  19995  issrngd  20830  quscrng  21279  mamudm  22381  mat1dimcrng  22463  mavmuldm  22536  fitop  22886  tgcl  22955  topbas  22958  ppttop  22993  epttop  22995  restbas  23144  isnrm2  23344  isnrm3  23345  2ndcctbss  23441  txbas  23553  txbasval  23592  txhaus  23633  xkohaus  23639  basqtop  23697  opnfbas  23828  isfild  23844  filfi  23845  neifil  23866  fbasrn  23870  filufint  23906  rnelfmlem  23938  fmfnfmlem3  23942  fmfnfm  23944  blfps  24392  blf  24393  blbas  24416  minveclem3b  25416  aalioulem2  26320  nocvxmin  27767  negsprop  28047  axcontlem9  29061  upgrwlkdvdelem  29824  grpodivf  30629  ipf  30804  ocsh  31374  adjadj  32027  unopadj2  32029  hmopadj  32030  hmopbdoptHIL  32079  lnopmi  32091  adjlnop  32177  xreceu  33002  esumcocn  34274  bnj1384  35227  f1resrcmplf1d  35281  mclsax  35810  dfon2  36031  outsideofeu  36372  hilbert1.2  36396  opnrebl2  36562  nn0prpw  36564  fness  36590  tailfb  36618  ontopbas  36669  neificl  38133  metf1o  38135  crngohomfo  38386  smprngopr  38432  ispridlc  38450  disjdmqsss  39285  disjdmqscossss  39286  eldisjs6  39320  prter2  39386  snatpsubN  40255  pclclN  40396  pclfinN  40405  ltrncnv  40651  cdleme24  40857  cdleme28  40878  cdleme50ltrn  41062  cdleme  41065  ltrnco  41224  cdlemk28-3  41413  diaf11N  41554  dibf11N  41666  dihlsscpre  41739  mapdpg  42211  mapdh9a  42294  mapdh9aOLDN  42295  hdmap14lem6  42378  mzpincl  43196  mzpindd  43208  iunconnlem2  45391  islptre  46076  ormkglobd  47332  fcoresf1  47544  2reu8i  47588  lmod1  48995