Theorem ralrimivva 2559

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
ralrimivva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)

Assertion

Ref	Expression
ralrimivva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Distinct variable groups:   𝜑,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)
2	1	ex 115	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 2558	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∀wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  swopo  4306  sosng  4699  fcof1  5783  fliftfund  5797  isoresbr  5809  isocnv  5811  f1oiso  5826  oveqrspc2v  5901  caovclg  6026  caovcomg  6029  off  6094  caofrss  6106  oprssdmm  6171  dmmpog  6209  fnmpoovd  6215  fmpoco  6216  poxp  6232  f1od2  6235  eroprf  6627  dom2lem  6771  xpf1o  6843  fidifsnid  6870  nnwetri  6914  undiffi  6923  fidcenumlemim  6950  supmoti  6991  supsnti  7003  supisoti  7008  difinfsnlem  7097  nninfwlpor  7171  netap  7252  2omotaplemap  7255  cc2lem  7264  addlocpr  7534  mullocpr  7569  cauappcvgprlemloc  7650  cauappcvgprlemlim  7659  caucvgprlemloc  7673  caucvgprprlemloc  7701  suplocexprlemloc  7719  suplocsrlemb  7804  rereceu  7887  axpre-suploclemres  7899  ltordlem  8437  cju  8916  exbtwnz  10248  frec2uzf1od  10403  frec2uzisod  10404  frecuzrdgrrn  10405  frec2uzrdg  10406  frecuzrdgrcl  10407  frecuzrdgsuc  10411  frecuzrdgrclt  10412  frecuzrdgg  10413  frecuzrdgsuctlem  10420  seqvalcd  10456  seqovcd  10460  seq3caopr3  10478  seq3caopr2  10479  iseqf1olemqf1o  10490  seq3homo  10507  seq3distr  10510  fimaxq  10802  zfz1isolem1  10815  rsqrmo  11031  climcn2  11312  addcn2  11313  mulcn2  11315  fsum2dlemstep  11437  fisumcom2  11441  cvgratnn  11534  fprodcl2lem  11608  fprod2dlemstep  11625  fprodcom2fi  11629  divalglemeunn  11920  divalglemeuneg  11922  bezoutlemeu  12002  isprm6  12141  pw2dvdseu  12162  crth  12218  eulerthlemh  12225  ennnfonelemim  12419  nninfdclemf1  12447  unbendc  12449  imasaddfnlemg  12729  ercpbl  12744  plusffng  12778  mgmplusf  12779  opifismgmdc  12784  ismndd  12832  mndpropd  12835  issubmnd  12837  mndinvmod  12840  mhmpropd  12851  idmhm  12854  mhmf1o  12855  issubmd  12859  mndissubm  12860  submid  12862  0mhm  12867  mhmco  12868  grppropd  12887  grpsubf  12943  dfgrp3m  12963  mhmmnd  12974  mhmfmhm  12975  mulgfng  12981  issubg4m  13046  grpissubg  13047  isnsg3  13060  0nsg  13067  nsgid  13068  srgfcl  13149  srglmhm  13169  srgrmhm  13170  aprap  13337  issubrg2  13362  subrgintm  13364  tgclb  13496  txbas  13689  txcnp  13702  txcnmpt  13704  cnmpt21  13722  txswaphmeo  13752  isxmetd  13778  isxmet2d  13779  xmettpos  13801  blfvalps  13816  xmetresbl  13871  metss2  13929  comet  13930  bdmet  13933  bdmopn  13935  xmetxp  13938  qtopbasss  13952  elcncf1di  13997  cncfcdm  14000  mulc1cncf  14007  cncfco  14009  dedekindeulemloc  14028  dedekindeu  14032  dedekindicclemloc  14037  dedekindicclemicc  14041  ivthinclemloc  14050  sssneq  14671  exmidsbthrlem  14690  cvgcmp2n  14701  trirec0  14712  apdiff  14716  redc0  14725  reap0  14726  neap0mkv  14736