Theorem rexlimdvaa 3164

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypothesis

Ref	Expression
rexlimdvaa.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
rexlimdvaa	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvaa

Step	Hyp	Ref	Expression
1		rexlimdvaa.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
2	1	expr 462	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 3163	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:  rexlimddv  3169  tz7.7  6388  isofrlem  7349  fnwe2lem3  8150  nnawordex  8650  nnaordex2  8652  oaabs2  8662  fiin  9418  marypha1lem  9429  wemaplem3  9546  cantnflt  9677  fseqenlem2  10108  cardaleph  10172  coftr  10355  fin23lem26  10407  fin1a2lem13  10494  fpwwe2  10732  r1wunlim  10826  wunex2  10827  inttsk  10863  grur1  10909  inaprc  10925  receu  11965  zsupss  13068  xralrple  13339  rexanuz  15519  limsupval2  15653  caucvgb  15853  fsumiun  15994  rpnnen2lem12  16399  dvdsval2  16431  prmind2  16866  prmdvdsncoprmbd  16909  pcprmpw2  17066  pockthg  17090  prmreclem5  17104  vdwlem6  17170  vdwlem10  17174  sscpwex  17996  drsdirfi  18485  0gisid  18854  psgnunilem3  19716  sylow3lem2  19848  efgsfo  19959  lt6abl  20115  ghmcyg  20116  ablsimpgfind  20332  unitgrp  20619  irredrmul  20663  unichnlidl  21522  drngnidl  21537  znunit  21875  matunitlindflem1  23000  tgcl  23293  neiint  23428  restopnb  23499  ordtrest2lem  23527  pnfnei  23544  mnfnei  23545  iscnp4  23587  haust1  23676  ordthauslem  23707  tgcmp  23725  t1connperf  23760  2ndc1stc  23775  2ndcdisj  23781  islly2  23809  nllyrest  23811  reftr  23839  comppfsc  23857  ptbasfi  23906  ptcnp  23947  xkococnlem  23984  tgqtop  24037  fbssfi  24162  fgabs  24204  neifil  24205  trfil2  24212  elfm2  24273  elfm3  24275  rnelfmlem  24277  fmfnfmlem4  24282  flffbas  24320  fclsfnflim  24352  ptcmplem4  24380  tsmsxp  24480  blssexps  24751  blssex  24752  icccmplem3  25150  cnheibor  25282  pi1blem  25366  iscfil3  25600  iscmet3lem2  25619  metsscmetcld  25642  ovolicc2  25849  nulmbl2  25863  volsup  25883  dyadmbllem  25926  itg2const2  26068  bddmulibl  26165  bddiblnc  26168  limcflf  26207  itgsubst  26375  ulmdvlem3  26735  xrlimcnp  27302  amgm  27324  dchrptlem2  27598  lgsne0  27668  lgsqr  27684  lgsquadlem1  27713  dchrvmasumif  27836  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lem3  27852  dchrisum0  27853  dchrmusum  27857  dchrvmasum  27858  chpdifbnd  27888  pntrlog2bnd  27917  pntibndlem3  27925  pntibnd  27926  pntleml  27944  ostth  27972  nosupno  28066  nosupbnd1lem1  28071  nosupbnd2  28079  noinfno  28081  noinfbnd1lem1  28086  noinfbnd2  28094  cutbdaybnd2  28188  oldlim  28279  oldbdayim  28281  leadds1  28381  norecdiv  28582  precsexlem11  28609  noseqrdgfn  28698  pw2recs  28830  z12sge0  28875  brbtwn2  29489  colinearalg  29494  nbumgrvtx  29933  cusgrfilem1  30042  nmobndi  31383  spansneleq  32178  ofrn2  33282  xreceu  33535  ordtrest2NEWlem  34601  dya2iocnei  34961  dfac16  35811  connpconn  36087  cvmsss2  36126  cvmlift2lem10  36164  cvmlift3lem2  36172  outsidele  36990  ltnadd  37060  nadddilem4  37065  neibastop1  37240  neibastop2lem  37241  ttctr  37374  dfttc2g  37387  dfttc4  37411  mblfinlem1  38669  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  cnambfre  38680  itg2addnclem  38683  itg2addnclem3  38685  ftc1anclem7  38711  ftc1anc  38713  fdc  38773  sstotbnd2  38802  sstotbnd  38803  isbndx  38810  ssbnd  38816  totbndbnd  38817  heibor  38849  unichnidl  39059  pexmidlem8N  41128  sn-0tie0  43609  elrfi  43799  hbtlem5  44224  rexlimdvaacbv  45297  rexlimddvcbvw  45298  relpfrlem  46037  liminfval2  46872  2zrngamgm  49436