Theorem ralrimivv 3204

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3078

This theorem is referenced by:  ralrimivva  3206  ralrimdvv  3207  reuind  3715  disjiund  5099  disjxiun  5105  somo  5608  ssrel2  5771  sorpsscmpl  7731  resf1extb  7930  f1o2ndf1  8116  soxp  8124  smoiso  8348  smo11  8350  fiint  9285  sornom  10260  axdc4lem  10438  zorn2lem6  10484  fpwwe2lem11  10625  fpwwe2lem12  10626  nqereu  10913  genpnnp  10989  receu  11858  lbreu  12164  injresinj  13819  sqrmo  15301  iscatd  17728  isfuncd  17921  0subm  18875  insubm  18876  sursubmefmnd  18954  injsubmefmnd  18955  cycsubm  19272  symgextf1  19490  lsmsubm  19722  iscmnd  19863  qusabl  19934  cycsubmcmn  19958  dprdsubg  20095  issrngd  20937  quscrng  21402  mamudm  22531  mat1dimcrng  22613  mavmuldm  22686  fitop  23036  tgcl  23105  topbas  23108  ppttop  23143  epttop  23145  restbas  23294  isnrm2  23494  isnrm3  23495  2ndcctbss  23591  txbas  23703  txbasval  23742  txhaus  23783  xkohaus  23789  basqtop  23847  opnfbas  23978  isfild  23994  filfi  23995  neifil  24016  fbasrn  24020  filufint  24056  rnelfmlem  24088  fmfnfmlem3  24092  fmfnfm  24094  blfps  24542  blf  24543  blbas  24566  minveclem3b  25566  aalioulem2  26473  nocvxmin  27924  negsprop  28204  axcontlem9  29288  upgrwlkdvdelem  30051  grpodivf  30856  ipf  31031  ocsh  31601  adjadj  32254  unopadj2  32256  hmopadj  32257  hmopbdoptHIL  32306  lnopmi  32318  adjlnop  32404  xreceu  33207  esumcocn  34436  bnj1384  35386  f1resrcmplf1d  35440  mclsax  36015  dfon2  36236  outsideofeu  36577  hilbert1.2  36601  opnrebl2  36776  nn0prpw  36778  fness  36804  tailfb  36832  ontopbas  36883  neificl  38348  metf1o  38350  crngohomfo  38601  smprngopr  38647  ispridlc  38665  disjdmqsss  39500  disjdmqscossss  39501  eldisjs6  39535  prter2  39601  snatpsubN  40470  pclclN  40611  pclfinN  40620  ltrncnv  40866  cdleme24  41072  cdleme28  41093  cdleme50ltrn  41277  cdleme  41280  ltrnco  41439  cdlemk28-3  41628  diaf11N  41769  dibf11N  41881  dihlsscpre  41954  mapdpg  42426  mapdh9a  42509  mapdh9aOLDN  42510  hdmap14lem6  42593  mzpincl  43413  mzpindd  43425  iunconnlem2  45591  islptre  46283  ormkglobd  47539  fcoresf1  47751  2reu8i  47795  smprngprmrng  49049  lmod1  49217