Theorem rexlimdvva 3225

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  rexlimdvvva  3226  disjxiun  5111  reuop  6301  f1prex  7293  f1o2ndf1  8126  poxp2  8148  xpord2pred  8150  sexp2  8151  xpord3pred  8157  sexp3  8158  frrlem9  8300  uniinqs  8804  eroveu  8819  eroprf  8822  ralxpmap  8903  unxpdomlem3  9228  finsschain  9326  dffi3  9401  sornom  10279  genpv  11002  genpdm  11005  1re  11226  cnegex  11409  zaddcl  12652  rexanre  15424  o1lo1  15614  lo1resb  15641  o1resb  15643  rlimcn3  15667  climcn2  15670  o1of2  15690  o1rlimmul  15696  lo1add  15704  lo1mul  15705  summo  15794  o1fsum  15891  ntrivcvgmul  15982  prodmolem2  16015  prodmo  16016  dvds2lem  16351  bezoutlem4  16625  dvdsmulgcd  16639  divgcdcoprm0  16748  cncongr1  16750  pcqmul  16938  pcneg  16959  pcadd  16974  4sqlem1  17033  4sqlem2  17034  4sqlem4  17037  mul4sq  17039  4sqlem12  17041  4sqlem13  17042  4sqlem18  17047  vdwmc2  17064  vdwlem7  17072  vdwlem9  17074  vdwlem10  17075  vdwlem11  17076  ramlb  17104  ramub1lem2  17112  imasaddfnlem  17607  imasmnd2  18863  xpsmnd0  18867  imasgrp2  19152  cyccom  19305  gaorber  19409  psgnunilem2  19596  psgneu  19607  lsmsubm  19754  lsmsubg  19755  lsmmod  19776  lsmdisj2  19783  pj1eu  19797  efgtlen  19827  efgredlem  19848  efgredeu  19853  efgcpbllemb  19856  frgpuptinv  19872  frgpup3lem  19878  qusabl  19966  frgpnabllem1  19974  frgpnabl  19976  dprdsubg  20127  ablfacrp  20169  pgpfac1lem3  20180  imasrng  20286  imasring  20445  xpsring1d  20448  dvdsrtr  20483  isnzr2  20652  lss1d  21121  lsmcl  21241  lsmelval2  21243  lbsextlem2  21320  qsssubdrg  21613  znfld  21747  cygznlem3  21756  psgnghm  21767  lsmcss  21879  psdmul  22366  mdetunilem7  22812  mdetunilem8  22813  cayleyhamilton0  23083  cayleyhamiltonALT  23085  restbas  23352  ordtbas2  23385  ordtbas  23386  cnhaus  23548  cldllycmp  23689  txbas  23761  ptbasin  23771  txcls  23798  xkoccn  23813  txindis  23828  txlly  23830  txnlly  23831  pthaus  23832  ptrescn  23833  txhaus  23841  tx1stc  23844  txkgen  23846  xkohaus  23847  xkoptsub  23848  xkopt  23849  xkoco1cn  23851  xkoco2cn  23852  xkoinjcn  23881  fmfnfmlem3  24150  fmfnfmlem4  24151  hausflimi  24174  hauspwpwf1  24181  txflf  24200  qustgplem  24315  blin2  24623  prdsxmslem2  24723  xrge0tsms  25029  addcnlem  25059  minveclem3b  25624  pmltpc  25646  evthicc2  25656  dyaddisj  25792  ismbfd  25835  mbfimaopnlem  25851  rolle  26186  dvcnvrelem1  26213  dvcvx  26216  itgsubst  26245  plyf  26392  plypf1  26406  plyadd  26411  plymul  26412  coeeu  26419  dgrlem  26423  coeid  26432  aalioulem6  26537  logbgcd1irr  26996  o1cxp  27176  dchrptlem2  27466  lgsdchr  27556  2sqlem5  27623  2sqlem9  27628  2sqb  27633  2sqreulem1  27647  2sqreunnlem1  27650  2sqreunnltblem  27652  pntlemp  27811  pnt3  27813  ostthlem1  27828  ostth3  27839  nosupprefixmo  27901  noinfprefixmo  27902  addsproplem2  28200  negsproplem2  28259  mulsproplem9  28354  sltmuls1  28377  sltmuls2  28378  precsexlem8  28444  precsexlem9  28445  precsexlem10  28446  precsexlem11  28447  onmulscl  28508  eucliddivs  28606  zaddscl  28624  zmulscld  28627  z12addscl  28707  z12sge0  28713  recut  28724  readdscl  28729  remulscl  28732  axcontlem4  29354  axcontlem9  29359  upgrpredgv  29526  edglnl  29530  numedglnl  29531  usgredg4  29604  nbuhgr2vtx1edgb  29739  2pthon3v  30329  umgr3v3e3cycl  30572  3cyclfrgr  30676  n4cyclfrgr  30679  frgrwopreg  30711  2clwwlk2clwwlk  30738  ubthlem3  31261  cdjreui  32821  cdj3i  32830  br8d  32990  xrofsup  33149  xrge0tsmsd  33424  qqhval2  34403  mbfmco2  34687  txpconn  35745  cvmlift2lem10  35825  cvmlift2lem12  35827  cvmlift3lem7  35838  cvmlift3lem8  35839  satfv0  35871  satfv0fun  35884  satffunlem2lem1  35917  mclsppslem  36096  br8  36269  br6  36270  br4  36271  brsegle  36621  ltnmul  36729  nadddilem1  36733  tailfb  36929  unbdqndv2  37141  qdiff  38012  mblfinlem3  38351  ismblfin  38353  itg2addnc  38366  ftc1anc  38393  isbnd2  38475  isbnd3  38476  ssbnd  38480  ispridlc  38762  lshpkrlem6  39930  athgt  40271  3dim1  40282  3dim2  40283  lvolex3N  40353  llncvrlpln2  40372  lplncvrlvol2  40430  linepsubN  40567  lncvrelatN  40596  linepsubclN  40766  sn-negex12  43219  fidomncyc  43344  fsuppind  43363  flt4lem7  43432  nna4b4nsq  43433  eldioph2  43534  eldioph2b  43535  diophin  43544  diophun  43545  fphpdo  43585  irrapxlem3  43592  irrapxlem5  43594  pell1234qrne0  43621  pell1234qrreccl  43622  pell1234qrmulcl  43623  pell14qrgt0  43627  pell14qrdich  43637  pell1qrge1  43638  pell1qrgap  43642  pellqrex  43647  rmxycomplete  43685  jm2.27  43776  stoweidlem49  46804  m1modmmod  48142  ichreuopeq  48263  prproropf1olem2  48294  prproropf1olem4  48296  paireqne  48301  reupr  48312  nprmmul2  48318  nprmdvdsfacm1  48417  requad2  48429  gbowgt5  48568  isgrtri  48749  grimgrtri  48755  usgrgrtrirex  48756  gpgvtx0  48859  gpgvtx1  48860  gpgedgvtx0  48867  gpgedgvtx1  48868  pgn4cyclex  48932  prelrrx2b  49535