Theorem ralrimivva 2590

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2178  ∀wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  swopo  4371  sosng  4766  fcof1  5875  fliftfund  5889  isoresbr  5901  isocnv  5903  f1oiso  5918  oveqrspc2v  5994  caovclg  6122  caovcomg  6125  off  6194  caofrss  6213  caofdig  6215  oprssdmm  6280  dmmpog  6318  fnmpoovd  6324  fmpoco  6325  poxp  6341  f1od2  6344  eroprf  6738  dom2lem  6886  xpf1o  6966  fidifsnid  6994  nnwetri  7039  undiffi  7048  fidcenumlemim  7080  supmoti  7121  supsnti  7133  supisoti  7138  difinfsnlem  7227  nninfwlpor  7302  netap  7401  2omotaplemap  7404  cc2lem  7413  addlocpr  7684  mullocpr  7719  cauappcvgprlemloc  7800  cauappcvgprlemlim  7809  caucvgprlemloc  7823  caucvgprprlemloc  7851  suplocexprlemloc  7869  suplocsrlemb  7954  rereceu  8037  axpre-suploclemres  8049  ltordlem  8590  cju  9069  exbtwnz  10430  frec2uzf1od  10588  frec2uzisod  10589  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgg  10598  frecuzrdgsuctlem  10605  seqvalcd  10643  seqovcd  10649  seq3caopr3  10673  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemqf1o  10688  seq3homo  10709  seqhomog  10712  seqfeq4g  10713  seq3distr  10714  fimaxq  11009  zfz1isolem1  11022  wrd2ind  11214  rsqrmo  11453  climcn2  11735  addcn2  11736  mulcn2  11738  fsum2dlemstep  11860  fisumcom2  11864  cvgratnn  11957  fprodcl2lem  12031  fprod2dlemstep  12048  fprodcom2fi  12052  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemeu  12443  isprm6  12584  pw2dvdseu  12605  crth  12661  eulerthlemh  12668  4sqlemffi  12834  ennnfonelemim  12910  nninfdclemf1  12938  unbendc  12940  imasaddfnlemg  13261  ercpbl  13278  plusffng  13312  mgmplusf  13313  opifismgmdc  13318  issgrpd  13359  sgrppropd  13360  ismndd  13384  mndpropd  13387  issubmnd  13389  mndinvmod  13392  mhmpropd  13413  idmhm  13416  mhmf1o  13417  issubmd  13421  mndissubm  13422  submid  13424  0mhm  13433  resmhm  13434  resmhm2  13435  resmhm2b  13436  mhmco  13437  grppropd  13464  grpsubf  13526  dfgrp3m  13546  mhmmnd  13567  mhmfmhm  13568  mulgfng  13575  issubg4m  13644  grpissubg  13645  isnsg3  13658  0nsg  13665  nsgid  13666  isghmd  13703  ghmmhm  13704  idghm  13710  ghmnsgima  13719  ghmnsgpreima  13720  ghmf1  13724  kerf1ghm  13725  ghmf1o  13726  ghmcmn  13778  invghm  13780  ablnsg  13785  imasabl  13787  srgfcl  13850  srglmhm  13870  srgrmhm  13871  isrhm2d  14042  subrngringnsg  14082  issubrng2  14087  subrngintm  14089  issubrg2  14118  subrgintm  14120  aprap  14163  islmodd  14170  lmodscaf  14187  lmodprop2d  14225  islssmd  14236  islss4  14259  lsspropdg  14308  issubrgd  14329  dflidl2rng  14358  rnglidlmmgm  14373  expghmap  14484  mulgghm2  14485  znf1o  14528  znidom  14534  tgclb  14652  txbas  14845  txcnp  14858  txcnmpt  14860  cnmpt21  14878  txswaphmeo  14908  isxmetd  14934  isxmet2d  14935  xmettpos  14957  blfvalps  14972  xmetresbl  15027  metss2  15085  comet  15086  bdmet  15089  bdmopn  15091  xmetxp  15094  qtopbasss  15108  elcncf1di  15166  cncfcdm  15169  mulc1cncf  15176  cncfco  15178  dedekindeulemloc  15206  dedekindeu  15210  dedekindicclemloc  15215  dedekindicclemicc  15219  ivthinclemloc  15228  dich0  15239  dvmptfsum  15312  mpodvdsmulf1o  15577  fsumdvdsmul  15578  gausslemma2dlem1f1o  15652  lgseisenlem2  15663  lgsquadlemsfi  15667  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  sssneq  16141  exmidsbthrlem  16163  cvgcmp2n  16174  trirec0  16185  apdiff  16189  redc0  16198  reap0  16199  cndcap  16200  neap0mkv  16210