Theorem rexlimdvva 3223

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

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

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 1945

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

This theorem is used by:  rexlimdvvva  3224  disjxiun  5103  reuop  6317  f1prex  7318  f1o2ndf1  8163  poxp2  8190  xpord2pred  8192  sexp2  8193  xpord3pred  8199  sexp3  8200  frrlem9  8343  uniinqs  8849  eroveu  8864  eroprf  8867  ralxpmap  8955  unxpdomlem3  9280  finsschain  9379  dffi3  9453  sornom  10385  genpv  11114  genpdm  11117  1re  11338  cnegex  11521  zaddcl  12766  rexanre  15546  o1lo1  15736  lo1resb  15763  o1resb  15765  rlimcn3  15789  climcn2  15792  o1of2  15812  o1rlimmul  15818  lo1add  15826  lo1mul  15827  summo  15915  o1fsum  16012  ntrivcvgmul  16103  prodmolem2  16134  prodmo  16135  dvds2lem  16470  bezoutlem4  16747  dvdsmulgcd  16762  divgcdcoprm0  16872  cncongr1  16874  pcqmul  17063  pcneg  17084  pcadd  17099  4sqlem1  17158  4sqlem2  17159  4sqlem4  17162  mul4sq  17164  4sqlem12  17166  4sqlem13  17167  4sqlem18  17172  vdwmc2  17189  vdwlem7  17197  vdwlem9  17199  vdwlem10  17200  vdwlem11  17201  ramlb  17229  ramub1lem2  17237  imasaddfnlem  17732  imasmnd2  19000  xpsmnd0  19004  imasgrp2  19297  cyccom  19450  gaorber  19555  psgnunilem2  19742  psgneu  19753  lsmsubm  19900  lsmsubg  19901  lsmmod  19922  lsmdisj2  19929  pj1eu  19943  efgtlen  19973  efgredlem  19994  efgredeu  19999  efgcpbllemb  20002  frgpuptinv  20018  frgpup3lem  20024  qusabl  20112  frgpnabllem1  20120  frgpnabl  20122  dprdsubg  20273  ablfacrp  20315  pgpfac1lem3  20326  imasrng  20432  imasring  20593  xpsring1d  20596  dvdsrtr  20631  isnzr2  20801  lss1d  21271  lsmcl  21391  lsmelval2  21393  lbsextlem2  21470  qsssubdrg  21765  znfld  21899  cygznlem3  21908  psgnghm  21919  lsmcss  22031  psdmul  22520  mdetunilem7  22966  mdetunilem8  22967  cayleyhamilton0  23240  cayleyhamiltonALT  23242  restbas  23509  ordtbas2  23542  ordtbas  23543  cnhaus  23705  cldllycmp  23847  txbas  23919  ptbasin  23929  txcls  23956  xkoccn  23971  txindis  23986  txlly  23988  txnlly  23989  pthaus  23990  ptrescn  23991  txhaus  23999  tx1stc  24002  txkgen  24004  xkohaus  24005  xkoptsub  24006  xkopt  24007  xkoco1cn  24009  xkoco2cn  24010  xkoinjcn  24039  fmfnfmlem3  24308  fmfnfmlem4  24309  hausflimi  24332  hauspwpwf1  24339  txflf  24358  qustgplem  24473  blin2  24781  prdsxmslem2  24881  xrge0tsms  25187  addcnlem  25217  minveclem3b  25782  pmltpc  25804  evthicc2  25814  dyaddisj  25950  ismbfd  25993  mbfimaopnlem  26009  rolle  26343  dvcnvrelem1  26370  dvcvx  26373  itgsubst  26402  plyf  26549  plypf1  26564  plyadd  26569  plymul  26570  coeeu  26577  dgrlem  26581  coeid  26590  aalioulem6  26697  logbgcd1irr  27155  o1cxp  27335  dchrptlem2  27625  lgsdchr  27715  2sqlem5  27782  2sqlem9  27787  2sqb  27792  2sqreulem1  27806  2sqreunnlem1  27809  2sqreunnltblem  27811  pntlemp  27970  pnt3  27972  ostthlem1  27987  ostth3  27998  flt4lem7  28022  nna4b4nsq  28023  nosupprefixmo  28090  noinfprefixmo  28091  addsproplem2  28389  negsproplem2  28448  mulsproplem9  28543  sltmuls1  28566  sltmuls2  28567  precsexlem8  28633  precsexlem9  28634  precsexlem10  28635  precsexlem11  28636  onmulscl  28697  eucliddivs  28795  zaddscl  28813  zmulscld  28816  z12addscl  28896  z12sge0  28902  recut  28913  readdscl  28918  remulscl  28921  axcontlem4  29578  axcontlem9  29583  upgrpredgv  29750  edglnl  29754  numedglnl  29755  usgredg4  29831  nbuhgr2vtx1edgb  29966  2pthon3v  30565  umgr3v3e3cycl  30818  3cyclfrgr  30922  n4cyclfrgr  30925  frgrwopreg  30957  2clwwlk2clwwlk  30984  ubthlem3  31507  cdjreui  33067  cdj3i  33076  inagcgratrgncol  33090  br8d  33277  xrofsup  33432  xrge0tsmsd  33710  qqhval2  34697  mbfmco2  34980  txpconn  36177  cvmlift2lem10  36257  cvmlift2lem12  36259  cvmlift3lem7  36270  cvmlift3lem8  36271  satfv0  36303  satfv0fun  36316  satffunlem2lem1  36349  mclsppslem  36528  br8  36712  br6  36713  br4  36714  brsegle  37064  ltnmul  37156  nadddilem1  37160  tailfb  37356  unbdqndv2  37568  qdiff  38453  mblfinlem3  38782  ismblfin  38784  itg2addnc  38797  ftc1anc  38824  isbnd2  38920  isbnd3  38921  ssbnd  38925  ispridlc  39207  lshpkrlem6  40375  athgt  40716  3dim1  40727  3dim2  40728  lvolex3N  40798  llncvrlpln2  40817  lplncvrlvol2  40875  linepsubN  41012  lncvrelatN  41041  linepsubclN  41211  sn-negex12  43672  fidomncyc  43803  fsuppind  43822  eldioph2  43977  eldioph2b  43978  diophin  43987  diophun  43988  fphpdo  44028  irrapxlem3  44035  irrapxlem5  44037  pell1234qrne0  44064  pell1234qrreccl  44065  pell1234qrmulcl  44066  pell14qrgt0  44070  pell14qrdich  44080  pell1qrge1  44081  pell1qrgap  44085  pellqrex  44090  rmxycomplete  44128  jm2.27  44219  mpoexwd  46129  stoweidlem49  47274  m1modmmod  48649  ichreuopeq  48770  prproropf1olem2  48801  prproropf1olem4  48803  paireqne  48808  reupr  48819  nprmmul2  48825  nprmdvdsfacm1  48924  requad2  48936  gbowgt5  49075  isgrtri  49256  grimgrtri  49262  usgrgrtrirex  49263  gpgvtx0  49366  gpgvtx1  49367  gpgedgvtx0  49374  gpgedgvtx1  49375  pgn4cyclex  49439