Theorem rexlimdvaa 3213

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexlimddv  3219  tz7.7  6277  isofrlem  7191  nnawordex  8430  oaabs2  8439  fiin  9111  marypha1lem  9122  wemaplem3  9237  cantnflt  9360  fseqenlem2  9712  cardaleph  9776  coftr  9960  fin23lem26  10012  fin1a2lem13  10099  fpwwe2  10330  r1wunlim  10424  wunex2  10425  inttsk  10461  grur1  10507  inaprc  10523  receu  11550  zsupss  12606  xralrple  12868  rexanuz  14985  limsupval2  15117  caucvgb  15319  fsumiun  15461  rpnnen2lem12  15862  dvdsval2  15894  prmind2  16318  prmdvdsncoprmbd  16359  pcprmpw2  16511  pockthg  16535  prmreclem5  16549  vdwlem6  16615  vdwlem10  16619  sscpwex  17444  drsdirfi  17938  psgnunilem3  19019  sylow3lem2  19148  efgsfo  19260  lt6abl  19411  ghmcyg  19412  ablsimpgfind  19628  unitgrp  19824  irredrmul  19864  drngnidl  20413  znunit  20683  tgcl  22027  neiint  22163  restopnb  22234  ordtrest2lem  22262  pnfnei  22279  mnfnei  22280  iscnp4  22322  haust1  22411  ordthauslem  22442  tgcmp  22460  t1connperf  22495  2ndc1stc  22510  2ndcdisj  22515  islly2  22543  nllyrest  22545  reftr  22573  comppfsc  22591  ptbasfi  22640  ptcnp  22681  xkococnlem  22718  tgqtop  22771  fbssfi  22896  fgabs  22938  neifil  22939  trfil2  22946  elfm2  23007  elfm3  23009  rnelfmlem  23011  fmfnfmlem4  23016  flffbas  23054  fclsfnflim  23086  ptcmplem4  23114  tsmsxp  23214  blssexps  23487  blssex  23488  icccmplem3  23893  cnheibor  24024  pi1blem  24108  iscfil3  24342  iscmet3lem2  24361  metsscmetcld  24384  ovolicc2  24591  nulmbl2  24605  volsup  24625  dyadmbllem  24668  itg2const2  24811  bddmulibl  24908  bddiblnc  24911  limcflf  24950  itgsubst  25118  ulmdvlem3  25466  xrlimcnp  26023  amgm  26045  dchrptlem2  26318  lgsne0  26388  lgsqr  26404  lgsquadlem1  26433  dchrvmasumif  26556  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem3  26572  dchrisum0  26573  dchrmusum  26577  dchrvmasum  26578  chpdifbnd  26608  pntrlog2bnd  26637  pntibndlem3  26645  pntibnd  26646  pntleml  26664  ostth  26692  brbtwn2  27176  colinearalg  27181  nbumgrvtx  27616  cusgrfilem1  27725  nmobndi  29038  spansneleq  29833  ofrn2  30878  xreceu  31098  ordtrest2NEWlem  31774  dya2iocnei  32149  connpconn  33097  cvmsss2  33136  cvmlift2lem10  33174  cvmlift3lem2  33182  nosupno  33833  nosupbnd1lem1  33838  nosupbnd2  33846  noinfno  33848  noinfbnd1lem1  33853  noinfbnd2  33861  scutbdaybnd2  33937  oldlim  33996  oldbdayim  33998  outsidele  34361  neibastop1  34475  neibastop2lem  34476  matunitlindflem1  35700  mblfinlem1  35741  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  cnambfre  35752  itg2addnclem  35755  itg2addnclem3  35757  ftc1anclem7  35783  ftc1anc  35785  fdc  35830  sstotbnd2  35859  sstotbnd  35860  isbndx  35867  ssbnd  35873  totbndbnd  35874  heibor  35906  unichnidl  36116  pexmidlem8N  37918  sn-0tie0  40342  nna4b4nsq  40413  elrfi  40432  fnwe2lem2  40792  hbtlem5  40869  rexlimdvaacbv  41705  rexlimddvcbvw  41706  liminfval2  43199  2zrngamgm  45385