Theorem rexlimdvaa 3168

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 3167	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:  rexlimddv  3173  tz7.7  6412  isofrlem  7377  fnwe2lem3  8182  nnawordex  8682  nnaordex2  8684  oaabs2  8694  fiin  9449  marypha1lem  9460  wemaplem3  9577  cantnflt  9708  fseqenlem2  10141  cardaleph  10205  coftr  10388  fin23lem26  10440  fin1a2lem13  10527  fpwwe2  10765  r1wunlim  10859  wunex2  10860  inttsk  10896  grur1  10942  inaprc  10958  receu  11999  zsupss  13102  xralrple  13373  rexanuz  15554  limsupval2  15688  caucvgb  15888  fsumiun  16029  rpnnen2lem12  16434  dvdsval2  16466  prmind2  16901  prmdvdsncoprmbd  16944  pcprmpw2  17101  pockthg  17125  prmreclem5  17139  vdwlem6  17205  vdwlem10  17209  sscpwex  18031  drsdirfi  18520  0gisid  18889  psgnunilem3  19752  sylow3lem2  19884  efgsfo  19995  lt6abl  20151  ghmcyg  20152  ablsimpgfind  20368  unitgrp  20655  irredrmul  20699  unichnlidl  21558  drngnidl  21573  znunit  21913  matunitlindflem1  23038  tgcl  23331  neiint  23466  restopnb  23537  ordtrest2lem  23565  pnfnei  23582  mnfnei  23583  iscnp4  23625  haust1  23714  ordthauslem  23745  tgcmp  23763  t1connperf  23798  2ndc1stc  23813  2ndcdisj  23819  islly2  23847  nllyrest  23849  reftr  23877  comppfsc  23895  ptbasfi  23944  ptcnp  23985  xkococnlem  24022  tgqtop  24075  fbssfi  24200  fgabs  24242  neifil  24243  trfil2  24250  elfm2  24311  elfm3  24313  rnelfmlem  24315  fmfnfmlem4  24320  flffbas  24358  fclsfnflim  24390  ptcmplem4  24418  tsmsxp  24518  blssexps  24789  blssex  24790  icccmplem3  25188  cnheibor  25320  pi1blem  25404  iscfil3  25638  iscmet3lem2  25657  metsscmetcld  25680  ovolicc2  25887  nulmbl2  25901  volsup  25921  dyadmbllem  25964  itg2const2  26106  bddmulibl  26203  bddiblnc  26206  limcflf  26245  itgsubst  26413  ulmdvlem3  26775  xrlimcnp  27342  amgm  27364  dchrptlem2  27638  lgsne0  27708  lgsqr  27724  lgsquadlem1  27753  dchrvmasumif  27876  rpvmasum2  27885  dchrisum0re  27886  dchrisum0lem3  27892  dchrisum0  27893  dchrmusum  27897  dchrvmasum  27898  chpdifbnd  27928  pntrlog2bnd  27957  pntibndlem3  27965  pntibnd  27966  pntleml  27984  ostth  28012  nosupno  28106  nosupbnd1lem1  28111  nosupbnd2  28119  noinfno  28121  noinfbnd1lem1  28126  noinfbnd2  28134  cutbdaybnd2  28228  oldlim  28319  oldbdayim  28321  leadds1  28421  norecdiv  28622  precsexlem11  28649  noseqrdgfn  28738  pw2recs  28870  z12sge0  28915  brbtwn2  29529  colinearalg  29534  nbumgrvtx  29973  cusgrfilem1  30082  nmobndi  31423  spansneleq  32218  ofrn2  33322  xreceu  33574  ordtrest2NEWlem  34658  dya2iocnei  35018  dfac16  35880  connpconn  36201  cvmsss2  36240  cvmlift2lem10  36278  cvmlift3lem2  36286  outsidele  37105  ltnadd  37175  nadddilem4  37180  neibastop1  37355  neibastop2lem  37356  ttctr  37489  dfttc2g  37502  dfttc4  37526  mblfinlem1  38836  mblfinlem3  38838  mblfinlem4  38839  ismblfin  38840  cnambfre  38847  itg2addnclem  38850  itg2addnclem3  38852  ftc1anclem7  38878  ftc1anc  38880  fdc  38938  sstotbnd2  38967  sstotbnd  38968  isbndx  38975  ssbnd  38981  totbndbnd  38982  heibor  39014  unichnidl  39224  pexmidlem8N  41293  sn-0tie0  43775  elrfi  43965  hbtlem5  44389  rexlimdvaacbv  45458  rexlimddvcbvw  45459  relpfrlem  46201  liminfval2  47045  2zrngamgm  49609