Theorem rexlimdvva 3219

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexlimdvvva  3220  disjxiun  5099  reuop  6296  f1prex  7292  f1o2ndf1  8135  poxp2  8162  xpord2pred  8164  sexp2  8165  xpord3pred  8171  sexp3  8172  frrlem9  8315  uniinqs  8821  eroveu  8836  eroprf  8839  ralxpmap  8927  unxpdomlem3  9252  finsschain  9351  dffi3  9426  sornom  10358  genpv  11087  genpdm  11090  1re  11311  cnegex  11494  zaddcl  12739  rexanre  15519  o1lo1  15709  lo1resb  15736  o1resb  15738  rlimcn3  15762  climcn2  15765  o1of2  15785  o1rlimmul  15791  lo1add  15799  lo1mul  15800  summo  15888  o1fsum  15985  ntrivcvgmul  16076  prodmolem2  16107  prodmo  16108  dvds2lem  16443  bezoutlem4  16720  dvdsmulgcd  16735  divgcdcoprm0  16845  cncongr1  16847  pcqmul  17036  pcneg  17057  pcadd  17072  4sqlem1  17131  4sqlem2  17132  4sqlem4  17135  mul4sq  17137  4sqlem12  17139  4sqlem13  17140  4sqlem18  17145  vdwmc2  17162  vdwlem7  17170  vdwlem9  17172  vdwlem10  17173  vdwlem11  17174  ramlb  17202  ramub1lem2  17210  imasaddfnlem  17705  imasmnd2  18973  xpsmnd0  18977  imasgrp2  19270  cyccom  19423  gaorber  19527  psgnunilem2  19714  psgneu  19725  lsmsubm  19872  lsmsubg  19873  lsmmod  19894  lsmdisj2  19901  pj1eu  19915  efgtlen  19945  efgredlem  19966  efgredeu  19971  efgcpbllemb  19974  frgpuptinv  19990  frgpup3lem  19996  qusabl  20084  frgpnabllem1  20092  frgpnabl  20094  dprdsubg  20245  ablfacrp  20287  pgpfac1lem3  20298  imasrng  20404  imasring  20565  xpsring1d  20568  dvdsrtr  20603  isnzr2  20773  lss1d  21243  lsmcl  21363  lsmelval2  21365  lbsextlem2  21442  qsssubdrg  21737  znfld  21871  cygznlem3  21880  psgnghm  21891  lsmcss  22003  psdmul  22492  mdetunilem7  22938  mdetunilem8  22939  cayleyhamilton0  23212  cayleyhamiltonALT  23214  restbas  23481  ordtbas2  23514  ordtbas  23515  cnhaus  23677  cldllycmp  23819  txbas  23891  ptbasin  23901  txcls  23928  xkoccn  23943  txindis  23958  txlly  23960  txnlly  23961  pthaus  23962  ptrescn  23963  txhaus  23971  tx1stc  23974  txkgen  23976  xkohaus  23977  xkoptsub  23978  xkopt  23979  xkoco1cn  23981  xkoco2cn  23982  xkoinjcn  24011  fmfnfmlem3  24280  fmfnfmlem4  24281  hausflimi  24304  hauspwpwf1  24311  txflf  24330  qustgplem  24445  blin2  24753  prdsxmslem2  24853  xrge0tsms  25159  addcnlem  25189  minveclem3b  25754  pmltpc  25776  evthicc2  25786  dyaddisj  25922  ismbfd  25965  mbfimaopnlem  25981  rolle  26315  dvcnvrelem1  26342  dvcvx  26345  itgsubst  26374  plyf  26521  plypf1  26536  plyadd  26541  plymul  26542  coeeu  26549  dgrlem  26553  coeid  26562  aalioulem6  26669  logbgcd1irr  27127  o1cxp  27307  dchrptlem2  27597  lgsdchr  27687  2sqlem5  27754  2sqlem9  27759  2sqb  27764  2sqreulem1  27778  2sqreunnlem1  27781  2sqreunnltblem  27783  pntlemp  27942  pnt3  27944  ostthlem1  27959  ostth3  27970  flt4lem7  27994  nna4b4nsq  27995  nosupprefixmo  28062  noinfprefixmo  28063  addsproplem2  28361  negsproplem2  28420  mulsproplem9  28515  sltmuls1  28538  sltmuls2  28539  precsexlem8  28605  precsexlem9  28606  precsexlem10  28607  precsexlem11  28608  onmulscl  28669  eucliddivs  28767  zaddscl  28785  zmulscld  28788  z12addscl  28868  z12sge0  28874  recut  28885  readdscl  28890  remulscl  28893  axcontlem4  29550  axcontlem9  29555  upgrpredgv  29722  edglnl  29726  numedglnl  29727  usgredg4  29803  nbuhgr2vtx1edgb  29938  2pthon3v  30537  umgr3v3e3cycl  30790  3cyclfrgr  30894  n4cyclfrgr  30897  frgrwopreg  30929  2clwwlk2clwwlk  30956  ubthlem3  31479  cdjreui  33039  cdj3i  33048  inagcgratrgncol  33062  br8d  33249  xrofsup  33405  xrge0tsmsd  33680  qqhval2  34660  mbfmco2  34943  txpconn  36083  cvmlift2lem10  36163  cvmlift2lem12  36165  cvmlift3lem7  36176  cvmlift3lem8  36177  satfv0  36209  satfv0fun  36222  satffunlem2lem1  36255  mclsppslem  36434  br8  36613  br6  36614  br4  36615  brsegle  36965  ltnmul  37057  nadddilem1  37061  tailfb  37257  unbdqndv2  37469  qdiff  38341  mblfinlem3  38670  ismblfin  38672  itg2addnc  38685  ftc1anc  38712  isbnd2  38810  isbnd3  38811  ssbnd  38815  ispridlc  39097  lshpkrlem6  40265  athgt  40606  3dim1  40617  3dim2  40618  lvolex3N  40688  llncvrlpln2  40707  lplncvrlvol2  40765  linepsubN  40902  lncvrelatN  40931  linepsubclN  41101  sn-negex12  43561  fidomncyc  43692  fsuppind  43711  eldioph2  43866  eldioph2b  43867  diophin  43876  diophun  43877  fphpdo  43917  irrapxlem3  43924  irrapxlem5  43926  pell1234qrne0  43953  pell1234qrreccl  43954  pell1234qrmulcl  43955  pell14qrgt0  43959  pell14qrdich  43969  pell1qrge1  43970  pell1qrgap  43974  pellqrex  43979  rmxycomplete  44017  jm2.27  44108  stoweidlem49  47152  m1modmmod  48527  ichreuopeq  48648  prproropf1olem2  48679  prproropf1olem4  48681  paireqne  48686  reupr  48697  nprmmul2  48703  nprmdvdsfacm1  48802  requad2  48814  gbowgt5  48953  isgrtri  49134  grimgrtri  49140  usgrgrtrirex  49141  gpgvtx0  49244  gpgvtx1  49245  gpgedgvtx0  49252  gpgedgvtx1  49253  pgn4cyclex  49317