Theorem rexlimdvva 3186

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvvva  3187  disjxiun  5092  reuop  6245  f1prex  7225  f1o2ndf1  8062  poxp2  8083  xpord2pred  8085  sexp2  8086  xpord3pred  8092  sexp3  8093  frrlem9  8234  uniinqs  8731  eroveu  8746  eroprf  8749  ralxpmap  8830  unxpdomlem3  9157  finsschain  9268  dffi3  9340  sornom  10190  genpv  10912  genpdm  10915  1re  11134  cnegex  11315  zaddcl  12533  rexanre  15272  o1lo1  15462  lo1resb  15489  o1resb  15491  rlimcn3  15515  climcn2  15518  o1of2  15538  o1rlimmul  15544  lo1add  15552  lo1mul  15553  summo  15642  o1fsum  15738  ntrivcvgmul  15827  prodmolem2  15860  prodmo  15861  dvds2lem  16197  bezoutlem4  16471  dvdsmulgcd  16485  divgcdcoprm0  16594  cncongr1  16596  pcqmul  16783  pcneg  16804  pcadd  16819  4sqlem1  16878  4sqlem2  16879  4sqlem4  16882  mul4sq  16884  4sqlem12  16886  4sqlem13  16887  4sqlem18  16892  vdwmc2  16909  vdwlem7  16917  vdwlem9  16919  vdwlem10  16920  vdwlem11  16921  ramlb  16949  ramub1lem2  16957  imasaddfnlem  17450  imasmnd2  18666  xpsmnd0  18670  imasgrp2  18952  cyccom  19100  gaorber  19205  psgnunilem2  19392  psgneu  19403  lsmsubm  19550  lsmsubg  19551  lsmmod  19572  lsmdisj2  19579  pj1eu  19593  efgtlen  19623  efgredlem  19644  efgredeu  19649  efgcpbllemb  19652  frgpuptinv  19668  frgpup3lem  19674  qusabl  19762  frgpnabllem1  19770  frgpnabl  19772  dprdsubg  19923  ablfacrp  19965  pgpfac1lem3  19976  imasrng  20080  imasring  20233  xpsring1d  20236  dvdsrtr  20271  isnzr2  20421  lss1d  20884  lsmcl  21005  lsmelval2  21007  lbsextlem2  21084  qsssubdrg  21351  znfld  21485  cygznlem3  21494  psgnghm  21505  lsmcss  21617  psdmul  22069  mdetunilem7  22521  mdetunilem8  22522  cayleyhamilton0  22792  cayleyhamiltonALT  22794  restbas  23061  ordtbas2  23094  ordtbas  23095  cnhaus  23257  cldllycmp  23398  txbas  23470  ptbasin  23480  txcls  23507  xkoccn  23522  txindis  23537  txlly  23539  txnlly  23540  pthaus  23541  ptrescn  23542  txhaus  23550  tx1stc  23553  txkgen  23555  xkohaus  23556  xkoptsub  23557  xkopt  23558  xkoco1cn  23560  xkoco2cn  23561  xkoinjcn  23590  fmfnfmlem3  23859  fmfnfmlem4  23860  hausflimi  23883  hauspwpwf1  23890  txflf  23909  qustgplem  24024  blin2  24333  prdsxmslem2  24433  xrge0tsms  24739  addcnlem  24769  minveclem3b  25344  pmltpc  25367  evthicc2  25377  dyaddisj  25513  ismbfd  25556  mbfimaopnlem  25572  rolle  25910  dvcnvrelem1  25938  dvcvx  25941  itgsubst  25972  plyf  26119  plypf1  26133  plyadd  26138  plymul  26139  coeeu  26146  dgrlem  26150  coeid  26159  aalioulem6  26261  logbgcd1irr  26720  o1cxp  26901  dchrptlem2  27192  lgsdchr  27282  2sqlem5  27349  2sqlem9  27354  2sqb  27359  2sqreulem1  27373  2sqreunnlem1  27376  2sqreunnltblem  27378  pntlemp  27537  pnt3  27539  ostthlem1  27554  ostth3  27565  nosupprefixmo  27628  noinfprefixmo  27629  addsproplem2  27900  negsproplem2  27958  mulsproplem9  28050  ssltmul1  28073  ssltmul2  28074  precsexlem8  28139  precsexlem9  28140  precsexlem10  28141  precsexlem11  28142  onmulscl  28198  eucliddivs  28288  zaddscl  28305  zmulscld  28308  zs12addscl  28372  zs12ge0  28378  recut  28383  readdscl  28386  remulscl  28389  axcontlem4  28930  axcontlem9  28935  upgrpredgv  29102  edglnl  29106  numedglnl  29107  usgredg4  29180  nbuhgr2vtx1edgb  29315  2pthon3v  29906  umgr3v3e3cycl  30146  3cyclfrgr  30250  n4cyclfrgr  30253  frgrwopreg  30285  2clwwlk2clwwlk  30312  ubthlem3  30834  cdjreui  32394  cdj3i  32403  br8d  32571  xrofsup  32723  xrge0tsmsd  33028  qqhval2  33948  mbfmco2  34232  txpconn  35204  cvmlift2lem10  35284  cvmlift2lem12  35286  cvmlift3lem7  35297  cvmlift3lem8  35298  satfv0  35330  satfv0fun  35343  satffunlem2lem1  35376  mclsppslem  35555  br8  35728  br6  35729  br4  35730  brsegle  36081  tailfb  36350  unbdqndv2  36484  mblfinlem3  37638  ismblfin  37640  itg2addnc  37653  ftc1anc  37680  isbnd2  37762  isbnd3  37763  ssbnd  37767  ispridlc  38049  lshpkrlem6  39093  athgt  39435  3dim1  39446  3dim2  39447  lvolex3N  39517  llncvrlpln2  39536  lplncvrlvol2  39594  linepsubN  39731  lncvrelatN  39760  linepsubclN  39930  sn-negex12  42390  fidomncyc  42508  fsuppind  42563  flt4lem7  42632  nna4b4nsq  42633  eldioph2  42735  eldioph2b  42736  diophin  42745  diophun  42746  fphpdo  42790  irrapxlem3  42797  irrapxlem5  42799  pell1234qrne0  42826  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell14qrgt0  42832  pell14qrdich  42842  pell1qrge1  42843  pell1qrgap  42847  pellqrex  42852  rmxycomplete  42890  jm2.27  42981  stoweidlem49  46031  m1modmmod  47343  ichreuopeq  47458  prproropf1olem2  47489  prproropf1olem4  47491  paireqne  47496  reupr  47507  requad2  47608  gbowgt5  47747  isgrtri  47928  grimgrtri  47934  usgrgrtrirex  47935  gpgvtx0  48038  gpgvtx1  48039  gpgedgvtx0  48046  gpgedgvtx1  48047  pgn4cyclex  48111  prelrrx2b  48700