Theorem ralrimivva 2626

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∀wral 2522

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  swopo  4432  sosng  4828  fcof1  5962  fliftfund  5976  isoresbr  5988  isocnv  5990  f1oiso  6005  oveqrspc2v  6085  caovclg  6215  caovcomg  6218  off  6288  caofrss  6307  caofdig  6309  oprssdmm  6378  dmmpog  6418  fnmpoovd  6424  fmpoco  6425  poxp  6441  f1od2  6444  suppofss1dcl  6477  suppofss2dcl  6478  eroprf  6875  dom2lem  7024  xpf1o  7110  fidifsnid  7139  nnwetri  7189  undiffi  7198  fidcenumlemim  7235  supmoti  7297  supsnti  7309  supisoti  7314  difinfsnlem  7403  nninfwlpor  7478  netap  7584  2omotaplemap  7587  cc2lem  7596  addlocpr  7867  mullocpr  7902  cauappcvgprlemloc  7983  cauappcvgprlemlim  7992  caucvgprlemloc  8006  caucvgprprlemloc  8034  suplocexprlemloc  8052  suplocsrlemb  8137  rereceu  8220  axpre-suploclemres  8232  ltordlem  8773  cju  9252  exbtwnz  10634  frec2uzf1od  10792  frec2uzisod  10793  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seqvalcd  10847  seqovcd  10853  seq3caopr3  10877  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemqf1o  10892  seq3homo  10913  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  fimaxq  11219  zfz1isolem1  11237  wrd2ind  11440  rsqrmo  11737  climcn2  12019  addcn2  12020  mulcn2  12022  fsum2dlemstep  12145  fisumcom2  12149  cvgratnn  12242  fprodcl2lem  12316  fprod2dlemstep  12333  fprodcom2fi  12337  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemeu  12728  isprm6  12869  pw2dvdseu  12890  crth  12946  eulerthlemh  12953  4sqlemffi  13119  ennnfonelemim  13259  nninfdclemf1  13287  unbendc  13289  imasaddfnlemg  13578  ercpbl  13595  plusffng  13628  mgmplusf  13629  opifismgmdc  13634  issgrpd  13675  sgrppropd  13676  ismndd  13698  mndpropd  13701  issubmnd  13703  mndinvmod  13706  mhmpropd  13721  idmhm  13724  mhmf1o  13725  issubmd  13729  mndissubm  13730  submid  13732  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  mhmco  13745  grppropd  13772  grpsubf  13834  dfgrp3m  13854  mhmmnd  13869  mhmfmhm  13870  mulgfng  13877  issubg4m  13946  grpissubg  13947  isnsg3  13960  0nsg  13967  nsgid  13968  isghmd  14005  ghmmhm  14006  idghm  14012  ghmnsgima  14021  ghmnsgpreima  14022  ghmf1  14026  kerf1ghm  14027  ghmf1o  14028  ghmcmn  14080  invghm  14082  ablnsg  14087  imasabl  14089  srgfcl  14216  srglmhm  14236  srgrmhm  14237  isrhm2d  14410  subrngringnsg  14451  issubrng2  14456  subrngintm  14458  issubrg2  14487  subrgintm  14489  aprap  14536  aprlring  14538  islmodd  14567  lmodscaf  14584  lmodprop2d  14622  islssmd  14633  islss4  14656  lsspropdg  14705  issubrgd  14726  dflidl2rng  14755  rnglidlmmgm  14770  expghmap  14881  mulgghm2  14882  znf1o  14925  znidom  14931  tgclb  15056  txbas  15249  txcnp  15262  txcnmpt  15264  cnmpt21  15282  txswaphmeo  15312  isxmetd  15338  isxmet2d  15339  xmettpos  15361  blfvalps  15376  xmetresbl  15431  metss2  15489  comet  15490  bdmet  15493  bdmopn  15495  xmetxp  15498  qtopbasss  15512  elcncf1di  15570  cncfcdm  15573  mulc1cncf  15580  cncfco  15582  dedekindeulemloc  15610  dedekindeu  15614  dedekindicclemloc  15619  dedekindicclemicc  15623  ivthinclemloc  15632  dich0  15643  dvmptfsum  15716  mpodvdsmulf1o  15984  fsumdvdsmul  15985  gausslemma2dlem1f1o  16059  lgseisenlem2  16070  lgsquadlemsfi  16074  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  usgredgreu  16337  uspgredg2vtxeu  16339  uspgredg2v  16342  usgredg2v  16345  vtxedgfi  16410  vtxlpfi  16411  sssneq  16902  exmidsbthrlem  16928  cvgcmp2n  16943  trirec0  16954  apdiff  16958  redc0  16968  reap0  16969  cndcap  16970  trimul0or  16971  neap0mkv  16981