Theorem ralrimivv 3176

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ralrimivva  3178  ralrimdvv  3179  reuind  3696  disjiund  5065  disjxiun  5071  somo  5567  ssrel2  5730  sorpsscmpl  7677  resf1extb  7874  f1o2ndf1  8061  soxp  8068  smoiso  8291  smo11  8293  fiint  9226  sornom  10188  axdc4lem  10366  zorn2lem6  10412  fpwwe2lem11  10553  fpwwe2lem12  10554  nqereu  10841  genpnnp  10917  receu  11784  lbreu  12095  injresinj  13735  sqrmo  15202  iscatd  17628  isfuncd  17821  0subm  18774  insubm  18775  sursubmefmnd  18853  injsubmefmnd  18854  cycsubm  19166  symgextf1  19385  lsmsubm  19617  iscmnd  19758  qusabl  19829  cycsubmcmn  19853  dprdsubg  19990  issrngd  20821  quscrng  21270  mamudm  22348  mat1dimcrng  22430  mavmuldm  22503  fitop  22853  tgcl  22922  topbas  22925  ppttop  22960  epttop  22962  restbas  23111  isnrm2  23311  isnrm3  23312  2ndcctbss  23408  txbas  23520  txbasval  23559  txhaus  23600  xkohaus  23606  basqtop  23664  opnfbas  23795  isfild  23811  filfi  23812  neifil  23833  fbasrn  23837  filufint  23873  rnelfmlem  23905  fmfnfmlem3  23909  fmfnfm  23911  blfps  24359  blf  24360  blbas  24383  minveclem3b  25383  aalioulem2  26287  nocvxmin  27735  negsprop  28015  axcontlem9  29029  upgrwlkdvdelem  29792  grpodivf  30597  ipf  30772  ocsh  31342  adjadj  31995  unopadj2  31997  hmopadj  31998  hmopbdoptHIL  32047  lnopmi  32059  adjlnop  32145  xreceu  32969  esumcocn  34212  bnj1384  35162  f1resrcmplf1d  35218  mclsax  35739  dfon2  35960  outsideofeu  36301  hilbert1.2  36325  opnrebl2  36491  nn0prpw  36493  fness  36519  tailfb  36547  ontopbas  36598  neificl  38062  metf1o  38064  crngohomfo  38315  smprngopr  38361  ispridlc  38379  disjdmqsss  39214  disjdmqscossss  39215  eldisjs6  39249  prter2  39315  snatpsubN  40184  pclclN  40325  pclfinN  40334  ltrncnv  40580  cdleme24  40786  cdleme28  40807  cdleme50ltrn  40991  cdleme  40994  ltrnco  41153  cdlemk28-3  41342  diaf11N  41483  dibf11N  41595  dihlsscpre  41668  mapdpg  42140  mapdh9a  42223  mapdh9aOLDN  42224  hdmap14lem6  42307  mzpincl  43154  mzpindd  43166  iunconnlem2  45349  islptre  46037  ormkglobd  47293  fcoresf1  47505  2reu8i  47549  lmod1  48956