Theorem ralrimivva 2612

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  swopo  4401  sosng  4797  fcof1  5919  fliftfund  5933  isoresbr  5945  isocnv  5947  f1oiso  5962  oveqrspc2v  6040  caovclg  6170  caovcomg  6173  off  6243  caofrss  6262  caofdig  6264  oprssdmm  6329  dmmpog  6369  fnmpoovd  6375  fmpoco  6376  poxp  6392  f1od2  6395  eroprf  6792  dom2lem  6940  xpf1o  7025  fidifsnid  7053  nnwetri  7101  undiffi  7110  fidcenumlemim  7142  supmoti  7183  supsnti  7195  supisoti  7200  difinfsnlem  7289  nninfwlpor  7364  netap  7463  2omotaplemap  7466  cc2lem  7475  addlocpr  7746  mullocpr  7781  cauappcvgprlemloc  7862  cauappcvgprlemlim  7871  caucvgprlemloc  7885  caucvgprprlemloc  7913  suplocexprlemloc  7931  suplocsrlemb  8016  rereceu  8099  axpre-suploclemres  8111  ltordlem  8652  cju  9131  exbtwnz  10500  frec2uzf1od  10658  frec2uzisod  10659  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgsuctlem  10675  seqvalcd  10713  seqovcd  10719  seq3caopr3  10743  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemqf1o  10758  seq3homo  10779  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  fimaxq  11081  zfz1isolem1  11094  wrd2ind  11294  rsqrmo  11578  climcn2  11860  addcn2  11861  mulcn2  11863  fsum2dlemstep  11985  fisumcom2  11989  cvgratnn  12082  fprodcl2lem  12156  fprod2dlemstep  12173  fprodcom2fi  12177  divalglemeunn  12472  divalglemeuneg  12474  bezoutlemeu  12568  isprm6  12709  pw2dvdseu  12730  crth  12786  eulerthlemh  12793  4sqlemffi  12959  ennnfonelemim  13035  nninfdclemf1  13063  unbendc  13065  imasaddfnlemg  13387  ercpbl  13404  plusffng  13438  mgmplusf  13439  opifismgmdc  13444  issgrpd  13485  sgrppropd  13486  ismndd  13510  mndpropd  13513  issubmnd  13515  mndinvmod  13518  mhmpropd  13539  idmhm  13542  mhmf1o  13543  issubmd  13547  mndissubm  13548  submid  13550  0mhm  13559  resmhm  13560  resmhm2  13561  resmhm2b  13562  mhmco  13563  grppropd  13590  grpsubf  13652  dfgrp3m  13672  mhmmnd  13693  mhmfmhm  13694  mulgfng  13701  issubg4m  13770  grpissubg  13771  isnsg3  13784  0nsg  13791  nsgid  13792  isghmd  13829  ghmmhm  13830  idghm  13836  ghmnsgima  13845  ghmnsgpreima  13846  ghmf1  13850  kerf1ghm  13851  ghmf1o  13852  ghmcmn  13904  invghm  13906  ablnsg  13911  imasabl  13913  srgfcl  13976  srglmhm  13996  srgrmhm  13997  isrhm2d  14169  subrngringnsg  14209  issubrng2  14214  subrngintm  14216  issubrg2  14245  subrgintm  14247  aprap  14290  islmodd  14297  lmodscaf  14314  lmodprop2d  14352  islssmd  14363  islss4  14386  lsspropdg  14435  issubrgd  14456  dflidl2rng  14485  rnglidlmmgm  14500  expghmap  14611  mulgghm2  14612  znf1o  14655  znidom  14661  tgclb  14779  txbas  14972  txcnp  14985  txcnmpt  14987  cnmpt21  15005  txswaphmeo  15035  isxmetd  15061  isxmet2d  15062  xmettpos  15084  blfvalps  15099  xmetresbl  15154  metss2  15212  comet  15213  bdmet  15216  bdmopn  15218  xmetxp  15221  qtopbasss  15235  elcncf1di  15293  cncfcdm  15296  mulc1cncf  15303  cncfco  15305  dedekindeulemloc  15333  dedekindeu  15337  dedekindicclemloc  15342  dedekindicclemicc  15346  ivthinclemloc  15355  dich0  15366  dvmptfsum  15439  mpodvdsmulf1o  15704  fsumdvdsmul  15705  gausslemma2dlem1f1o  15779  lgseisenlem2  15790  lgsquadlemsfi  15794  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  usgredgreu  16055  uspgredg2vtxeu  16057  uspgredg2v  16060  usgredg2v  16063  vtxedgfi  16095  vtxlpfi  16096  sssneq  16539  exmidsbthrlem  16562  cvgcmp2n  16573  trirec0  16584  apdiff  16588  redc0  16597  reap0  16598  cndcap  16599  neap0mkv  16609