Theorem ralrimivva 2579

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  swopo  4342  sosng  4737  fcof1  5833  fliftfund  5847  isoresbr  5859  isocnv  5861  f1oiso  5876  oveqrspc2v  5952  caovclg  6080  caovcomg  6083  off  6152  caofrss  6171  caofdig  6173  oprssdmm  6238  dmmpog  6276  fnmpoovd  6282  fmpoco  6283  poxp  6299  f1od2  6302  eroprf  6696  dom2lem  6840  xpf1o  6914  fidifsnid  6941  nnwetri  6986  undiffi  6995  fidcenumlemim  7027  supmoti  7068  supsnti  7080  supisoti  7085  difinfsnlem  7174  nninfwlpor  7249  netap  7339  2omotaplemap  7342  cc2lem  7351  addlocpr  7622  mullocpr  7657  cauappcvgprlemloc  7738  cauappcvgprlemlim  7747  caucvgprlemloc  7761  caucvgprprlemloc  7789  suplocexprlemloc  7807  suplocsrlemb  7892  rereceu  7975  axpre-suploclemres  7987  ltordlem  8528  cju  9007  exbtwnz  10359  frec2uzf1od  10517  frec2uzisod  10518  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgsuctlem  10534  seqvalcd  10572  seqovcd  10578  seq3caopr3  10602  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemqf1o  10617  seq3homo  10638  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  fimaxq  10938  zfz1isolem1  10951  rsqrmo  11211  climcn2  11493  addcn2  11494  mulcn2  11496  fsum2dlemstep  11618  fisumcom2  11622  cvgratnn  11715  fprodcl2lem  11789  fprod2dlemstep  11806  fprodcom2fi  11810  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemeu  12201  isprm6  12342  pw2dvdseu  12363  crth  12419  eulerthlemh  12426  4sqlemffi  12592  ennnfonelemim  12668  nninfdclemf1  12696  unbendc  12698  imasaddfnlemg  13018  ercpbl  13035  plusffng  13069  mgmplusf  13070  opifismgmdc  13075  issgrpd  13116  sgrppropd  13117  ismndd  13141  mndpropd  13144  issubmnd  13146  mndinvmod  13149  mhmpropd  13170  idmhm  13173  mhmf1o  13174  issubmd  13178  mndissubm  13179  submid  13181  0mhm  13190  resmhm  13191  resmhm2  13192  resmhm2b  13193  mhmco  13194  grppropd  13221  grpsubf  13283  dfgrp3m  13303  mhmmnd  13324  mhmfmhm  13325  mulgfng  13332  issubg4m  13401  grpissubg  13402  isnsg3  13415  0nsg  13422  nsgid  13423  isghmd  13460  ghmmhm  13461  idghm  13467  ghmnsgima  13476  ghmnsgpreima  13477  ghmf1  13481  kerf1ghm  13482  ghmf1o  13483  ghmcmn  13535  invghm  13537  ablnsg  13542  imasabl  13544  srgfcl  13607  srglmhm  13627  srgrmhm  13628  isrhm2d  13799  subrngringnsg  13839  issubrng2  13844  subrngintm  13846  issubrg2  13875  subrgintm  13877  aprap  13920  islmodd  13927  lmodscaf  13944  lmodprop2d  13982  islssmd  13993  islss4  14016  lsspropdg  14065  issubrgd  14086  dflidl2rng  14115  rnglidlmmgm  14130  expghmap  14241  mulgghm2  14242  znf1o  14285  znidom  14291  tgclb  14409  txbas  14602  txcnp  14615  txcnmpt  14617  cnmpt21  14635  txswaphmeo  14665  isxmetd  14691  isxmet2d  14692  xmettpos  14714  blfvalps  14729  xmetresbl  14784  metss2  14842  comet  14843  bdmet  14846  bdmopn  14848  xmetxp  14851  qtopbasss  14865  elcncf1di  14923  cncfcdm  14926  mulc1cncf  14933  cncfco  14935  dedekindeulemloc  14963  dedekindeu  14967  dedekindicclemloc  14972  dedekindicclemicc  14976  ivthinclemloc  14985  dich0  14996  dvmptfsum  15069  mpodvdsmulf1o  15334  fsumdvdsmul  15335  gausslemma2dlem1f1o  15409  lgseisenlem2  15420  lgsquadlemsfi  15424  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  sssneq  15757  exmidsbthrlem  15779  cvgcmp2n  15790  trirec0  15801  apdiff  15805  redc0  15814  reap0  15815  cndcap  15816  neap0mkv  15826