Theorem ralrimivv 3178

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

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

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 3053

This theorem is referenced by:  ralrimivva  3180  ralrimdvv  3181  reuind  3712  disjiund  5090  disjxiun  5096  somo  5572  ssrel2  5735  sorpsscmpl  7681  resf1extb  7878  f1o2ndf1  8066  soxp  8073  smoiso  8296  smo11  8298  fiint  9231  sornom  10191  axdc4lem  10369  zorn2lem6  10415  fpwwe2lem11  10556  fpwwe2lem12  10557  nqereu  10844  genpnnp  10920  receu  11786  lbreu  12096  injresinj  13711  sqrmo  15178  iscatd  17600  isfuncd  17793  0subm  18746  insubm  18747  sursubmefmnd  18825  injsubmefmnd  18826  cycsubm  19135  symgextf1  19354  lsmsubm  19586  iscmnd  19727  qusabl  19798  cycsubmcmn  19822  dprdsubg  19959  issrngd  20792  quscrng  21242  mamudm  22343  mat1dimcrng  22425  mavmuldm  22498  fitop  22848  tgcl  22917  topbas  22920  ppttop  22955  epttop  22957  restbas  23106  isnrm2  23306  isnrm3  23307  2ndcctbss  23403  txbas  23515  txbasval  23554  txhaus  23595  xkohaus  23601  basqtop  23659  opnfbas  23790  isfild  23806  filfi  23807  neifil  23828  fbasrn  23832  filufint  23868  rnelfmlem  23900  fmfnfmlem3  23904  fmfnfm  23906  blfps  24354  blf  24355  blbas  24378  minveclem3b  25388  aalioulem2  26301  nocvxmin  27755  negsprop  28035  axcontlem9  29049  upgrwlkdvdelem  29813  grpodivf  30617  ipf  30792  ocsh  31362  adjadj  32015  unopadj2  32017  hmopadj  32018  hmopbdoptHIL  32067  lnopmi  32079  adjlnop  32165  xreceu  33005  esumcocn  34239  bnj1384  35190  f1resrcmplf1d  35245  mclsax  35765  dfon2  35986  outsideofeu  36327  hilbert1.2  36351  opnrebl2  36517  nn0prpw  36519  fness  36545  tailfb  36573  ontopbas  36624  neificl  37956  metf1o  37958  crngohomfo  38209  smprngopr  38255  ispridlc  38273  disjdmqsss  39108  disjdmqscossss  39109  eldisjs6  39143  prter2  39209  snatpsubN  40078  pclclN  40219  pclfinN  40228  ltrncnv  40474  cdleme24  40680  cdleme28  40701  cdleme50ltrn  40885  cdleme  40888  ltrnco  41047  cdlemk28-3  41236  diaf11N  41377  dibf11N  41489  dihlsscpre  41562  mapdpg  42034  mapdh9a  42117  mapdh9aOLDN  42118  hdmap14lem6  42201  mzpincl  43043  mzpindd  43055  iunconnlem2  45242  islptre  45932  ormkglobd  47186  fcoresf1  47382  2reu8i  47426  lmod1  48805