Theorem rexlimdvva 3195

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 412	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3194	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimdvvva  3196  disjxiun  5083  reuop  6251  f1prex  7232  f1o2ndf1  8065  poxp2  8086  xpord2pred  8088  sexp2  8089  xpord3pred  8095  sexp3  8096  frrlem9  8237  uniinqs  8737  eroveu  8752  eroprf  8755  ralxpmap  8837  unxpdomlem3  9161  finsschain  9262  dffi3  9337  sornom  10190  genpv  10913  genpdm  10916  1re  11135  cnegex  11318  zaddcl  12558  rexanre  15300  o1lo1  15490  lo1resb  15517  o1resb  15519  rlimcn3  15543  climcn2  15546  o1of2  15566  o1rlimmul  15572  lo1add  15580  lo1mul  15581  summo  15670  o1fsum  15767  ntrivcvgmul  15858  prodmolem2  15891  prodmo  15892  dvds2lem  16228  bezoutlem4  16502  dvdsmulgcd  16516  divgcdcoprm0  16625  cncongr1  16627  pcqmul  16815  pcneg  16836  pcadd  16851  4sqlem1  16910  4sqlem2  16911  4sqlem4  16914  mul4sq  16916  4sqlem12  16918  4sqlem13  16919  4sqlem18  16924  vdwmc2  16941  vdwlem7  16949  vdwlem9  16951  vdwlem10  16952  vdwlem11  16953  ramlb  16981  ramub1lem2  16989  imasaddfnlem  17483  imasmnd2  18733  xpsmnd0  18737  imasgrp2  19022  cyccom  19169  gaorber  19274  psgnunilem2  19461  psgneu  19472  lsmsubm  19619  lsmsubg  19620  lsmmod  19641  lsmdisj2  19648  pj1eu  19662  efgtlen  19692  efgredlem  19713  efgredeu  19718  efgcpbllemb  19721  frgpuptinv  19737  frgpup3lem  19743  qusabl  19831  frgpnabllem1  19839  frgpnabl  19841  dprdsubg  19992  ablfacrp  20034  pgpfac1lem3  20045  imasrng  20149  imasring  20301  xpsring1d  20304  dvdsrtr  20339  isnzr2  20486  lss1d  20949  lsmcl  21070  lsmelval2  21072  lbsextlem2  21149  qsssubdrg  21416  znfld  21550  cygznlem3  21559  psgnghm  21570  lsmcss  21682  psdmul  22142  mdetunilem7  22593  mdetunilem8  22594  cayleyhamilton0  22864  cayleyhamiltonALT  22866  restbas  23133  ordtbas2  23166  ordtbas  23167  cnhaus  23329  cldllycmp  23470  txbas  23542  ptbasin  23552  txcls  23579  xkoccn  23594  txindis  23609  txlly  23611  txnlly  23612  pthaus  23613  ptrescn  23614  txhaus  23622  tx1stc  23625  txkgen  23627  xkohaus  23628  xkoptsub  23629  xkopt  23630  xkoco1cn  23632  xkoco2cn  23633  xkoinjcn  23662  fmfnfmlem3  23931  fmfnfmlem4  23932  hausflimi  23955  hauspwpwf1  23962  txflf  23981  qustgplem  24096  blin2  24404  prdsxmslem2  24504  xrge0tsms  24810  addcnlem  24840  minveclem3b  25405  pmltpc  25427  evthicc2  25437  dyaddisj  25573  ismbfd  25616  mbfimaopnlem  25632  rolle  25967  dvcnvrelem1  25994  dvcvx  25997  itgsubst  26026  plyf  26173  plypf1  26187  plyadd  26192  plymul  26193  coeeu  26200  dgrlem  26204  coeid  26213  aalioulem6  26314  logbgcd1irr  26771  o1cxp  26952  dchrptlem2  27242  lgsdchr  27332  2sqlem5  27399  2sqlem9  27404  2sqb  27409  2sqreulem1  27423  2sqreunnlem1  27426  2sqreunnltblem  27428  pntlemp  27587  pnt3  27589  ostthlem1  27604  ostth3  27615  nosupprefixmo  27678  noinfprefixmo  27679  addsproplem2  27976  negsproplem2  28035  mulsproplem9  28130  sltmuls1  28153  sltmuls2  28154  precsexlem8  28220  precsexlem9  28221  precsexlem10  28222  precsexlem11  28223  onmulscl  28284  eucliddivs  28382  zaddscl  28400  zmulscld  28403  z12addscl  28483  z12sge0  28489  recut  28500  readdscl  28505  remulscl  28508  axcontlem4  29050  axcontlem9  29055  upgrpredgv  29222  edglnl  29226  numedglnl  29227  usgredg4  29300  nbuhgr2vtx1edgb  29435  2pthon3v  30026  umgr3v3e3cycl  30269  3cyclfrgr  30373  n4cyclfrgr  30376  frgrwopreg  30408  2clwwlk2clwwlk  30435  ubthlem3  30958  cdjreui  32518  cdj3i  32527  br8d  32696  xrofsup  32855  xrge0tsmsd  33149  qqhval2  34142  mbfmco2  34425  txpconn  35430  cvmlift2lem10  35510  cvmlift2lem12  35512  cvmlift3lem7  35523  cvmlift3lem8  35524  satfv0  35556  satfv0fun  35569  satffunlem2lem1  35602  mclsppslem  35781  br8  35954  br6  35955  br4  35956  brsegle  36306  tailfb  36575  unbdqndv2  36787  mblfinlem3  37994  ismblfin  37996  itg2addnc  38009  ftc1anc  38036  isbnd2  38118  isbnd3  38119  ssbnd  38123  ispridlc  38405  lshpkrlem6  39575  athgt  39916  3dim1  39927  3dim2  39928  lvolex3N  39998  llncvrlpln2  40017  lplncvrlvol2  40075  linepsubN  40212  lncvrelatN  40241  linepsubclN  40411  sn-negex12  42863  fidomncyc  42994  fsuppind  43037  flt4lem7  43106  nna4b4nsq  43107  eldioph2  43208  eldioph2b  43209  diophin  43218  diophun  43219  fphpdo  43263  irrapxlem3  43270  irrapxlem5  43272  pell1234qrne0  43299  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell14qrgt0  43305  pell14qrdich  43315  pell1qrge1  43316  pell1qrgap  43320  pellqrex  43325  rmxycomplete  43363  jm2.27  43454  stoweidlem49  46495  m1modmmod  47824  ichreuopeq  47945  prproropf1olem2  47976  prproropf1olem4  47978  paireqne  47983  reupr  47994  nprmmul2  48000  nprmdvdsfacm1  48099  requad2  48111  gbowgt5  48250  isgrtri  48431  grimgrtri  48437  usgrgrtrirex  48438  gpgvtx0  48541  gpgvtx1  48542  gpgedgvtx0  48549  gpgedgvtx1  48550  pgn4cyclex  48614  prelrrx2b  49202