Theorem rexlimdvaa 3214

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 457	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 3213	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexlimddv  3220  tz7.7  6292  isofrlem  7211  nnawordex  8468  oaabs2  8479  fiin  9181  marypha1lem  9192  wemaplem3  9307  cantnflt  9430  fseqenlem2  9781  cardaleph  9845  coftr  10029  fin23lem26  10081  fin1a2lem13  10168  fpwwe2  10399  r1wunlim  10493  wunex2  10494  inttsk  10530  grur1  10576  inaprc  10592  receu  11620  zsupss  12677  xralrple  12939  rexanuz  15057  limsupval2  15189  caucvgb  15391  fsumiun  15533  rpnnen2lem12  15934  dvdsval2  15966  prmind2  16390  prmdvdsncoprmbd  16431  pcprmpw2  16583  pockthg  16607  prmreclem5  16621  vdwlem6  16687  vdwlem10  16691  sscpwex  17527  drsdirfi  18023  psgnunilem3  19104  sylow3lem2  19233  efgsfo  19345  lt6abl  19496  ghmcyg  19497  ablsimpgfind  19713  unitgrp  19909  irredrmul  19949  drngnidl  20500  znunit  20771  tgcl  22119  neiint  22255  restopnb  22326  ordtrest2lem  22354  pnfnei  22371  mnfnei  22372  iscnp4  22414  haust1  22503  ordthauslem  22534  tgcmp  22552  t1connperf  22587  2ndc1stc  22602  2ndcdisj  22607  islly2  22635  nllyrest  22637  reftr  22665  comppfsc  22683  ptbasfi  22732  ptcnp  22773  xkococnlem  22810  tgqtop  22863  fbssfi  22988  fgabs  23030  neifil  23031  trfil2  23038  elfm2  23099  elfm3  23101  rnelfmlem  23103  fmfnfmlem4  23108  flffbas  23146  fclsfnflim  23178  ptcmplem4  23206  tsmsxp  23306  blssexps  23579  blssex  23580  icccmplem3  23987  cnheibor  24118  pi1blem  24202  iscfil3  24437  iscmet3lem2  24456  metsscmetcld  24479  ovolicc2  24686  nulmbl2  24700  volsup  24720  dyadmbllem  24763  itg2const2  24906  bddmulibl  25003  bddiblnc  25006  limcflf  25045  itgsubst  25213  ulmdvlem3  25561  xrlimcnp  26118  amgm  26140  dchrptlem2  26413  lgsne0  26483  lgsqr  26499  lgsquadlem1  26528  dchrvmasumif  26651  rpvmasum2  26660  dchrisum0re  26661  dchrisum0lem3  26667  dchrisum0  26668  dchrmusum  26672  dchrvmasum  26673  chpdifbnd  26703  pntrlog2bnd  26732  pntibndlem3  26740  pntibnd  26741  pntleml  26759  ostth  26787  brbtwn2  27273  colinearalg  27278  nbumgrvtx  27713  cusgrfilem1  27822  nmobndi  29137  spansneleq  29932  ofrn2  30977  xreceu  31196  ordtrest2NEWlem  31872  dya2iocnei  32249  connpconn  33197  cvmsss2  33236  cvmlift2lem10  33274  cvmlift3lem2  33282  nosupno  33906  nosupbnd1lem1  33911  nosupbnd2  33919  noinfno  33921  noinfbnd1lem1  33926  noinfbnd2  33934  scutbdaybnd2  34010  oldlim  34069  oldbdayim  34071  outsidele  34434  neibastop1  34548  neibastop2lem  34549  matunitlindflem1  35773  mblfinlem1  35814  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  cnambfre  35825  itg2addnclem  35828  itg2addnclem3  35830  ftc1anclem7  35856  ftc1anc  35858  fdc  35903  sstotbnd2  35932  sstotbnd  35933  isbndx  35940  ssbnd  35946  totbndbnd  35947  heibor  35979  unichnidl  36189  pexmidlem8N  37991  sn-0tie0  40421  nna4b4nsq  40497  elrfi  40516  fnwe2lem2  40876  hbtlem5  40953  rexlimdvaacbv  41816  rexlimddvcbvw  41817  liminfval2  43309  2zrngamgm  45497