Theorem ralrimivva 2588

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 2587	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  swopo  4354  sosng  4749  fcof1  5854  fliftfund  5868  isoresbr  5880  isocnv  5882  f1oiso  5897  oveqrspc2v  5973  caovclg  6101  caovcomg  6104  off  6173  caofrss  6192  caofdig  6194  oprssdmm  6259  dmmpog  6297  fnmpoovd  6303  fmpoco  6304  poxp  6320  f1od2  6323  eroprf  6717  dom2lem  6865  xpf1o  6943  fidifsnid  6970  nnwetri  7015  undiffi  7024  fidcenumlemim  7056  supmoti  7097  supsnti  7109  supisoti  7114  difinfsnlem  7203  nninfwlpor  7278  netap  7368  2omotaplemap  7371  cc2lem  7380  addlocpr  7651  mullocpr  7686  cauappcvgprlemloc  7767  cauappcvgprlemlim  7776  caucvgprlemloc  7790  caucvgprprlemloc  7818  suplocexprlemloc  7836  suplocsrlemb  7921  rereceu  8004  axpre-suploclemres  8016  ltordlem  8557  cju  9036  exbtwnz  10395  frec2uzf1od  10553  frec2uzisod  10554  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgsuctlem  10570  seqvalcd  10608  seqovcd  10614  seq3caopr3  10638  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemqf1o  10653  seq3homo  10674  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  fimaxq  10974  zfz1isolem1  10987  rsqrmo  11371  climcn2  11653  addcn2  11654  mulcn2  11656  fsum2dlemstep  11778  fisumcom2  11782  cvgratnn  11875  fprodcl2lem  11949  fprod2dlemstep  11966  fprodcom2fi  11970  divalglemeunn  12265  divalglemeuneg  12267  bezoutlemeu  12361  isprm6  12502  pw2dvdseu  12523  crth  12579  eulerthlemh  12586  4sqlemffi  12752  ennnfonelemim  12828  nninfdclemf1  12856  unbendc  12858  imasaddfnlemg  13179  ercpbl  13196  plusffng  13230  mgmplusf  13231  opifismgmdc  13236  issgrpd  13277  sgrppropd  13278  ismndd  13302  mndpropd  13305  issubmnd  13307  mndinvmod  13310  mhmpropd  13331  idmhm  13334  mhmf1o  13335  issubmd  13339  mndissubm  13340  submid  13342  0mhm  13351  resmhm  13352  resmhm2  13353  resmhm2b  13354  mhmco  13355  grppropd  13382  grpsubf  13444  dfgrp3m  13464  mhmmnd  13485  mhmfmhm  13486  mulgfng  13493  issubg4m  13562  grpissubg  13563  isnsg3  13576  0nsg  13583  nsgid  13584  isghmd  13621  ghmmhm  13622  idghm  13628  ghmnsgima  13637  ghmnsgpreima  13638  ghmf1  13642  kerf1ghm  13643  ghmf1o  13644  ghmcmn  13696  invghm  13698  ablnsg  13703  imasabl  13705  srgfcl  13768  srglmhm  13788  srgrmhm  13789  isrhm2d  13960  subrngringnsg  14000  issubrng2  14005  subrngintm  14007  issubrg2  14036  subrgintm  14038  aprap  14081  islmodd  14088  lmodscaf  14105  lmodprop2d  14143  islssmd  14154  islss4  14177  lsspropdg  14226  issubrgd  14247  dflidl2rng  14276  rnglidlmmgm  14291  expghmap  14402  mulgghm2  14403  znf1o  14446  znidom  14452  tgclb  14570  txbas  14763  txcnp  14776  txcnmpt  14778  cnmpt21  14796  txswaphmeo  14826  isxmetd  14852  isxmet2d  14853  xmettpos  14875  blfvalps  14890  xmetresbl  14945  metss2  15003  comet  15004  bdmet  15007  bdmopn  15009  xmetxp  15012  qtopbasss  15026  elcncf1di  15084  cncfcdm  15087  mulc1cncf  15094  cncfco  15096  dedekindeulemloc  15124  dedekindeu  15128  dedekindicclemloc  15133  dedekindicclemicc  15137  ivthinclemloc  15146  dich0  15157  dvmptfsum  15230  mpodvdsmulf1o  15495  fsumdvdsmul  15496  gausslemma2dlem1f1o  15570  lgseisenlem2  15581  lgsquadlemsfi  15585  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  sssneq  15976  exmidsbthrlem  15998  cvgcmp2n  16009  trirec0  16020  apdiff  16024  redc0  16033  reap0  16034  cndcap  16035  neap0mkv  16045