Theorem rexlimdvva 3253

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdvva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))
2	1	ex 416	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3252	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  disjxiun  5027  reuop  6112  f1prex  7018  f1o2ndf1  7801  uniinqs  8360  eroveu  8375  eroprf  8378  ralxpmap  8443  unxpdomlem3  8708  finsschain  8815  dffi3  8879  sornom  9688  genpv  10410  genpdm  10413  1re  10630  cnegex  10810  zaddcl  12010  rexanre  14698  o1lo1  14886  lo1resb  14913  o1resb  14915  rlimcn2  14939  climcn2  14941  o1of2  14961  o1rlimmul  14967  lo1add  14975  lo1mul  14976  summo  15066  o1fsum  15160  ntrivcvgmul  15250  prodmolem2  15281  prodmo  15282  dvds2lem  15614  bezoutlem4  15880  dvdsmulgcd  15895  divgcdcoprm0  15999  cncongr1  16001  pcqmul  16180  pcneg  16200  pcadd  16215  4sqlem1  16274  4sqlem2  16275  4sqlem4  16278  mul4sq  16280  4sqlem12  16282  4sqlem13  16283  4sqlem18  16288  vdwmc2  16305  vdwlem7  16313  vdwlem9  16315  vdwlem10  16316  vdwlem11  16317  ramlb  16345  ramub1lem2  16353  imasaddfnlem  16793  imasmnd2  17940  imasgrp2  18206  cyccom  18338  gaorber  18430  psgnunilem2  18615  psgneu  18626  lsmsubm  18770  lsmsubg  18771  lsmmod  18793  lsmdisj2  18800  pj1eu  18814  efgtlen  18844  efgredlem  18865  efgredeu  18870  efgcpbllemb  18873  frgpuptinv  18889  frgpup3lem  18895  qusabl  18978  frgpnabllem1  18986  frgpnabl  18988  cygablOLD  19004  dprdsubg  19139  ablfacrp  19181  pgpfac1lem3  19192  imasring  19365  dvdsrtr  19398  lss1d  19728  lsmcl  19848  lsmelval2  19850  lbsextlem2  19924  isnzr2  20029  qsssubdrg  20150  znfld  20252  cygznlem3  20261  psgnghm  20269  lsmcss  20381  mdetunilem7  21223  mdetunilem8  21224  cayleyhamilton0  21494  cayleyhamiltonALT  21496  restbas  21763  ordtbas2  21796  ordtbas  21797  cnhaus  21959  cldllycmp  22100  txbas  22172  ptbasin  22182  txcls  22209  xkoccn  22224  txindis  22239  txlly  22241  txnlly  22242  pthaus  22243  ptrescn  22244  txhaus  22252  tx1stc  22255  txkgen  22257  xkohaus  22258  xkoptsub  22259  xkopt  22260  xkoco1cn  22262  xkoco2cn  22263  xkoinjcn  22292  fmfnfmlem3  22561  fmfnfmlem4  22562  hausflimi  22585  hauspwpwf1  22592  txflf  22611  qustgplem  22726  blin2  23036  prdsxmslem2  23136  xrge0tsms  23439  addcnlem  23469  minveclem3b  24032  pmltpc  24054  evthicc2  24064  dyaddisj  24200  ismbfd  24243  mbfimaopnlem  24259  rolle  24593  dvcnvrelem1  24620  dvcvx  24623  itgsubst  24652  plyf  24795  plypf1  24809  plyadd  24814  plymul  24815  coeeu  24822  dgrlem  24826  coeid  24835  aalioulem6  24933  logbgcd1irr  25380  o1cxp  25560  dchrptlem2  25849  lgsdchr  25939  2sqlem5  26006  2sqlem9  26011  2sqb  26016  2sqreulem1  26030  2sqreunnlem1  26033  2sqreunnltblem  26035  pntlemp  26194  pnt3  26196  ostthlem1  26211  ostth3  26222  axcontlem4  26761  axcontlem9  26766  upgrpredgv  26932  edglnl  26936  numedglnl  26937  usgredg4  27007  nbuhgr2vtx1edgb  27142  2pthon3v  27729  umgr3v3e3cycl  27969  3cyclfrgr  28073  n4cyclfrgr  28076  frgrwopreg  28108  2clwwlk2clwwlk  28135  ubthlem3  28655  cdjreui  30215  cdj3i  30224  br8d  30374  xrofsup  30518  xrge0tsmsd  30742  qqhval2  31333  mbfmco2  31633  txpconn  32592  cvmlift2lem10  32672  cvmlift2lem12  32674  cvmlift3lem7  32685  cvmlift3lem8  32686  satfv0  32718  satfv0fun  32731  satffunlem2lem1  32764  mclsppslem  32943  br8  33105  br6  33106  br4  33107  frrlem9  33244  noprefixmo  33315  brsegle  33682  tailfb  33838  unbdqndv2  33963  mblfinlem3  35096  ismblfin  35098  itg2addnc  35111  ftc1anc  35138  isbnd2  35221  isbnd3  35222  ssbnd  35226  ispridlc  35508  lshpkrlem6  36411  athgt  36752  3dim1  36763  3dim2  36764  lvolex3N  36834  llncvrlpln2  36853  lplncvrlvol2  36911  linepsubN  37048  lncvrelatN  37077  linepsubclN  37247  fsuppind  39456  sn-negex12  39553  eldioph2  39703  eldioph2b  39704  diophin  39713  diophun  39714  fphpdo  39758  irrapxlem3  39765  irrapxlem5  39767  pell1234qrne0  39794  pell1234qrreccl  39795  pell1234qrmulcl  39796  pell14qrgt0  39800  pell14qrdich  39810  pell1qrge1  39811  pell1qrgap  39815  pellqrex  39820  rmxycomplete  39858  jm2.27  39949  stoweidlem49  42691  ichreuopeq  43990  prproropf1olem2  44021  prproropf1olem4  44023  paireqne  44028  reupr  44039  requad2  44141  gbowgt5  44280  isomuspgrlem1  44345  isomuspgrlem2b  44347  isomuspgrlem2d  44349  m1modmmod  44935  prelrrx2b  45128