Theorem rexlimdvva 3210

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimdvvva  3211  disjxiun  5144  reuop  6314  f1prex  7303  f1o2ndf1  8145  poxp2  8166  xpord2pred  8168  sexp2  8169  xpord3pred  8175  sexp3  8176  frrlem9  8317  uniinqs  8835  eroveu  8850  eroprf  8853  ralxpmap  8934  unxpdomlem3  9285  finsschain  9396  dffi3  9468  sornom  10314  genpv  11036  genpdm  11039  1re  11258  cnegex  11439  zaddcl  12654  rexanre  15381  o1lo1  15569  lo1resb  15596  o1resb  15598  rlimcn3  15622  climcn2  15625  o1of2  15645  o1rlimmul  15651  lo1add  15659  lo1mul  15660  summo  15749  o1fsum  15845  ntrivcvgmul  15934  prodmolem2  15967  prodmo  15968  dvds2lem  16302  bezoutlem4  16575  dvdsmulgcd  16589  divgcdcoprm0  16698  cncongr1  16700  pcqmul  16886  pcneg  16907  pcadd  16922  4sqlem1  16981  4sqlem2  16982  4sqlem4  16985  mul4sq  16987  4sqlem12  16989  4sqlem13  16990  4sqlem18  16995  vdwmc2  17012  vdwlem7  17020  vdwlem9  17022  vdwlem10  17023  vdwlem11  17024  ramlb  17052  ramub1lem2  17060  imasaddfnlem  17574  imasmnd2  18799  xpsmnd0  18803  imasgrp2  19085  cyccom  19233  gaorber  19338  psgnunilem2  19527  psgneu  19538  lsmsubm  19685  lsmsubg  19686  lsmmod  19707  lsmdisj2  19714  pj1eu  19728  efgtlen  19758  efgredlem  19779  efgredeu  19784  efgcpbllemb  19787  frgpuptinv  19803  frgpup3lem  19809  qusabl  19897  frgpnabllem1  19905  frgpnabl  19907  dprdsubg  20058  ablfacrp  20100  pgpfac1lem3  20111  imasrng  20194  imasring  20343  xpsring1d  20346  dvdsrtr  20384  isnzr2  20534  lss1d  20978  lsmcl  21099  lsmelval2  21101  lbsextlem2  21178  qsssubdrg  21461  znfld  21596  cygznlem3  21605  psgnghm  21615  lsmcss  21727  psdmul  22187  mdetunilem7  22639  mdetunilem8  22640  cayleyhamilton0  22910  cayleyhamiltonALT  22912  restbas  23181  ordtbas2  23214  ordtbas  23215  cnhaus  23377  cldllycmp  23518  txbas  23590  ptbasin  23600  txcls  23627  xkoccn  23642  txindis  23657  txlly  23659  txnlly  23660  pthaus  23661  ptrescn  23662  txhaus  23670  tx1stc  23673  txkgen  23675  xkohaus  23676  xkoptsub  23677  xkopt  23678  xkoco1cn  23680  xkoco2cn  23681  xkoinjcn  23710  fmfnfmlem3  23979  fmfnfmlem4  23980  hausflimi  24003  hauspwpwf1  24010  txflf  24029  qustgplem  24144  blin2  24454  prdsxmslem2  24557  xrge0tsms  24869  addcnlem  24899  minveclem3b  25475  pmltpc  25498  evthicc2  25508  dyaddisj  25644  ismbfd  25687  mbfimaopnlem  25703  rolle  26042  dvcnvrelem1  26070  dvcvx  26073  itgsubst  26104  plyf  26251  plypf1  26265  plyadd  26270  plymul  26271  coeeu  26278  dgrlem  26282  coeid  26291  aalioulem6  26393  logbgcd1irr  26851  o1cxp  27032  dchrptlem2  27323  lgsdchr  27413  2sqlem5  27480  2sqlem9  27485  2sqb  27490  2sqreulem1  27504  2sqreunnlem1  27507  2sqreunnltblem  27509  pntlemp  27668  pnt3  27670  ostthlem1  27685  ostth3  27696  nosupprefixmo  27759  noinfprefixmo  27760  addsproplem2  28017  negsproplem2  28075  mulsproplem9  28164  ssltmul1  28187  ssltmul2  28188  precsexlem8  28252  precsexlem9  28253  precsexlem10  28254  precsexlem11  28255  onmulscl  28301  zaddscl  28394  zmulscld  28397  recut  28442  readdscl  28445  remulscl  28448  axcontlem4  28996  axcontlem9  29001  upgrpredgv  29170  edglnl  29174  numedglnl  29175  usgredg4  29248  nbuhgr2vtx1edgb  29383  2pthon3v  29972  umgr3v3e3cycl  30212  3cyclfrgr  30316  n4cyclfrgr  30319  frgrwopreg  30351  2clwwlk2clwwlk  30378  ubthlem3  30900  cdjreui  32460  cdj3i  32469  br8d  32629  xrofsup  32777  xrge0tsmsd  33047  qqhval2  33944  mbfmco2  34246  txpconn  35216  cvmlift2lem10  35296  cvmlift2lem12  35298  cvmlift3lem7  35309  cvmlift3lem8  35310  satfv0  35342  satfv0fun  35355  satffunlem2lem1  35388  mclsppslem  35567  br8  35735  br6  35736  br4  35737  brsegle  36089  tailfb  36359  unbdqndv2  36493  mblfinlem3  37645  ismblfin  37647  itg2addnc  37660  ftc1anc  37687  isbnd2  37769  isbnd3  37770  ssbnd  37774  ispridlc  38056  lshpkrlem6  39096  athgt  39438  3dim1  39449  3dim2  39450  lvolex3N  39520  llncvrlpln2  39539  lplncvrlvol2  39597  linepsubN  39734  lncvrelatN  39763  linepsubclN  39933  sn-negex12  42422  fidomncyc  42521  fsuppind  42576  flt4lem7  42645  nna4b4nsq  42646  eldioph2  42749  eldioph2b  42750  diophin  42759  diophun  42760  fphpdo  42804  irrapxlem3  42811  irrapxlem5  42813  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrgt0  42846  pell14qrdich  42856  pell1qrge1  42857  pell1qrgap  42861  pellqrex  42866  rmxycomplete  42905  jm2.27  42996  stoweidlem49  46004  ichreuopeq  47397  prproropf1olem2  47428  prproropf1olem4  47430  paireqne  47435  reupr  47446  requad2  47547  gbowgt5  47686  isgrtri  47847  grimgrtri  47851  usgrgrtrirex  47852  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  m1modmmod  48370  prelrrx2b  48563