Theorem ralrimivv 3199

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  ralrimivva  3201  ralrimdvv  3202  reuind  3758  disjiund  5133  disjxiun  5139  somo  5630  ssrel2  5794  sorpsscmpl  7755  resf1extb  7957  f1o2ndf1  8148  soxp  8155  smoiso  8403  smo11  8405  fiint  9367  fiintOLD  9368  sornom  10318  axdc4lem  10496  zorn2lem6  10542  fpwwe2lem11  10682  fpwwe2lem12  10683  nqereu  10970  genpnnp  11046  receu  11909  lbreu  12219  injresinj  13828  sqrmo  15291  iscatd  17717  isfuncd  17911  0subm  18831  insubm  18832  sursubmefmnd  18910  injsubmefmnd  18911  cycsubm  19221  symgextf1  19440  lsmsubm  19672  iscmnd  19813  qusabl  19884  cycsubmcmn  19908  dprdsubg  20045  issrngd  20857  quscrng  21294  mamudm  22400  mat1dimcrng  22484  mavmuldm  22557  fitop  22907  tgcl  22977  topbas  22980  ppttop  23015  epttop  23017  restbas  23167  isnrm2  23367  isnrm3  23368  2ndcctbss  23464  txbas  23576  txbasval  23615  txhaus  23656  xkohaus  23662  basqtop  23720  opnfbas  23851  isfild  23867  filfi  23868  neifil  23889  fbasrn  23893  filufint  23929  rnelfmlem  23961  fmfnfmlem3  23965  fmfnfm  23967  blfps  24417  blf  24418  blbas  24441  minveclem3b  25463  aalioulem2  26376  nocvxmin  27824  negsprop  28068  axcontlem9  28988  upgrwlkdvdelem  29757  grpodivf  30558  ipf  30733  ocsh  31303  adjadj  31956  unopadj2  31958  hmopadj  31959  hmopbdoptHIL  32008  lnopmi  32020  adjlnop  32106  xreceu  32905  esumcocn  34082  bnj1384  35047  f1resrcmplf1d  35102  mclsax  35575  dfon2  35794  outsideofeu  36133  hilbert1.2  36157  opnrebl2  36323  nn0prpw  36325  fness  36351  tailfb  36379  ontopbas  36430  neificl  37761  metf1o  37763  crngohomfo  38014  smprngopr  38060  ispridlc  38078  disjdmqsss  38804  disjdmqscossss  38805  prter2  38883  snatpsubN  39753  pclclN  39894  pclfinN  39903  ltrncnv  40149  cdleme24  40355  cdleme28  40376  cdleme50ltrn  40560  cdleme  40563  ltrnco  40722  cdlemk28-3  40911  diaf11N  41052  dibf11N  41164  dihlsscpre  41237  mapdpg  41709  mapdh9a  41792  mapdh9aOLDN  41793  hdmap14lem6  41876  mzpincl  42750  mzpindd  42762  iunconnlem2  44960  islptre  45639  ormkglobd  46895  fcoresf1  47086  2reu8i  47130  lmod1  48414