Theorem rexlimdvaa 3165

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

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

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 3088

This theorem is used by:  rexlimddv  3170  tz7.7  6387  isofrlem  7346  nnawordex  8639  nnaordex2  8641  oaabs2  8651  fiin  9407  marypha1lem  9418  wemaplem3  9535  cantnflt  9666  fseqenlem2  10097  cardaleph  10161  coftr  10344  fin23lem26  10396  fin1a2lem13  10483  fpwwe2  10721  r1wunlim  10815  wunex2  10816  inttsk  10852  grur1  10898  inaprc  10914  receu  11954  zsupss  13057  xralrple  13328  rexanuz  15506  limsupval2  15640  caucvgb  15840  fsumiun  15981  rpnnen2lem12  16386  dvdsval2  16418  prmind2  16853  prmdvdsncoprmbd  16896  pcprmpw2  17053  pockthg  17077  prmreclem5  17091  vdwlem6  17157  vdwlem10  17161  sscpwex  17983  drsdirfi  18472  0gisid  18841  psgnunilem3  19703  sylow3lem2  19835  efgsfo  19946  lt6abl  20102  ghmcyg  20103  ablsimpgfind  20319  unitgrp  20606  irredrmul  20650  unichnlidl  21509  drngnidl  21524  znunit  21862  matunitlindflem1  22987  tgcl  23280  neiint  23415  restopnb  23486  ordtrest2lem  23514  pnfnei  23531  mnfnei  23532  iscnp4  23574  haust1  23663  ordthauslem  23694  tgcmp  23712  t1connperf  23747  2ndc1stc  23762  2ndcdisj  23768  islly2  23796  nllyrest  23798  reftr  23826  comppfsc  23844  ptbasfi  23893  ptcnp  23934  xkococnlem  23971  tgqtop  24024  fbssfi  24149  fgabs  24191  neifil  24192  trfil2  24199  elfm2  24260  elfm3  24262  rnelfmlem  24264  fmfnfmlem4  24269  flffbas  24307  fclsfnflim  24339  ptcmplem4  24367  tsmsxp  24467  blssexps  24738  blssex  24739  icccmplem3  25137  cnheibor  25269  pi1blem  25353  iscfil3  25587  iscmet3lem2  25606  metsscmetcld  25629  ovolicc2  25836  nulmbl2  25850  volsup  25870  dyadmbllem  25913  itg2const2  26055  bddmulibl  26152  bddiblnc  26155  limcflf  26194  itgsubst  26362  ulmdvlem3  26722  xrlimcnp  27289  amgm  27311  dchrptlem2  27585  lgsne0  27655  lgsqr  27671  lgsquadlem1  27700  dchrvmasumif  27823  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem3  27839  dchrisum0  27840  dchrmusum  27844  dchrvmasum  27845  chpdifbnd  27875  pntrlog2bnd  27904  pntibndlem3  27912  pntibnd  27913  pntleml  27931  ostth  27959  nna4b4nsq  27983  nosupno  28053  nosupbnd1lem1  28058  nosupbnd2  28066  noinfno  28068  noinfbnd1lem1  28073  noinfbnd2  28081  cutbdaybnd2  28175  oldlim  28266  oldbdayim  28268  leadds1  28368  norecdiv  28569  precsexlem11  28596  noseqrdgfn  28685  pw2recs  28817  z12sge0  28862  brbtwn2  29476  colinearalg  29481  nbumgrvtx  29920  cusgrfilem1  30029  nmobndi  31370  spansneleq  32165  ofrn2  33227  xreceu  33481  ordtrest2NEWlem  34547  dya2iocnei  34907  connpconn  35979  cvmsss2  36018  cvmlift2lem10  36056  cvmlift3lem2  36064  outsidele  36877  ltnadd  36947  nadddilem4  36952  neibastop1  37127  neibastop2lem  37128  ttctr  37261  dfttc2g  37274  dfttc4  37298  mblfinlem1  38555  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  cnambfre  38566  itg2addnclem  38569  itg2addnclem3  38571  ftc1anclem7  38597  ftc1anc  38599  fdc  38659  sstotbnd2  38688  sstotbnd  38689  isbndx  38696  ssbnd  38702  totbndbnd  38703  heibor  38735  unichnidl  38945  pexmidlem8N  41014  sn-0tie0  43495  elrfi  43684  fnwe2lem2  44037  hbtlem5  44114  rexlimdvaacbv  45188  rexlimddvcbvw  45189  relpfrlem  45921  liminfval2  46747  2zrngamgm  49311