Theorem rexlimdvaa 3140

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimddv  3145  tz7.7  6343  isofrlem  7288  nnawordex  8566  nnaordex2  8568  oaabs2  8578  fiin  9328  marypha1lem  9339  wemaplem3  9456  cantnflt  9584  fseqenlem2  9938  cardaleph  10002  coftr  10186  fin23lem26  10238  fin1a2lem13  10325  fpwwe2  10557  r1wunlim  10651  wunex2  10652  inttsk  10688  grur1  10734  inaprc  10750  receu  11786  zsupss  12878  xralrple  13148  rexanuz  15299  limsupval2  15433  caucvgb  15633  fsumiun  15775  rpnnen2lem12  16183  dvdsval2  16215  prmind2  16645  prmdvdsncoprmbd  16688  pcprmpw2  16844  pockthg  16868  prmreclem5  16882  vdwlem6  16948  vdwlem10  16952  sscpwex  17773  drsdirfi  18262  psgnunilem3  19462  sylow3lem2  19594  efgsfo  19705  lt6abl  19861  ghmcyg  19862  ablsimpgfind  20078  unitgrp  20354  irredrmul  20398  drngnidl  21233  znunit  21553  tgcl  22944  neiint  23079  restopnb  23150  ordtrest2lem  23178  pnfnei  23195  mnfnei  23196  iscnp4  23238  haust1  23327  ordthauslem  23358  tgcmp  23376  t1connperf  23411  2ndc1stc  23426  2ndcdisj  23431  islly2  23459  nllyrest  23461  reftr  23489  comppfsc  23507  ptbasfi  23556  ptcnp  23597  xkococnlem  23634  tgqtop  23687  fbssfi  23812  fgabs  23854  neifil  23855  trfil2  23862  elfm2  23923  elfm3  23925  rnelfmlem  23927  fmfnfmlem4  23932  flffbas  23970  fclsfnflim  24002  ptcmplem4  24030  tsmsxp  24130  blssexps  24401  blssex  24402  icccmplem3  24800  cnheibor  24932  pi1blem  25016  iscfil3  25250  iscmet3lem2  25269  metsscmetcld  25292  ovolicc2  25499  nulmbl2  25513  volsup  25533  dyadmbllem  25576  itg2const2  25718  bddmulibl  25816  bddiblnc  25819  limcflf  25858  itgsubst  26026  ulmdvlem3  26380  xrlimcnp  26945  amgm  26968  dchrptlem2  27242  lgsne0  27312  lgsqr  27328  lgsquadlem1  27357  dchrvmasumif  27480  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem3  27496  dchrisum0  27497  dchrmusum  27501  dchrvmasum  27502  chpdifbnd  27532  pntrlog2bnd  27561  pntibndlem3  27569  pntibnd  27570  pntleml  27588  ostth  27616  nosupno  27681  nosupbnd1lem1  27686  nosupbnd2  27694  noinfno  27696  noinfbnd1lem1  27701  noinfbnd2  27709  cutbdaybnd2  27802  oldlim  27893  oldbdayim  27895  leadds1  27995  norecdiv  28196  precsexlem11  28223  noseqrdgfn  28312  pw2recs  28444  z12sge0  28489  brbtwn2  28988  colinearalg  28993  nbumgrvtx  29429  cusgrfilem1  29539  nmobndi  30861  spansneleq  31656  ofrn2  32728  xreceu  32996  ordtrest2NEWlem  34082  dya2iocnei  34442  connpconn  35433  cvmsss2  35472  cvmlift2lem10  35510  cvmlift3lem2  35518  outsidele  36330  neibastop1  36557  neibastop2lem  36558  ttctr  36691  dfttc2g  36704  dfttc4  36728  mh-inf3f1  36739  matunitlindflem1  37951  mblfinlem1  37992  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  cnambfre  38003  itg2addnclem  38006  itg2addnclem3  38008  ftc1anclem7  38034  ftc1anc  38036  fdc  38080  sstotbnd2  38109  sstotbnd  38110  isbndx  38117  ssbnd  38123  totbndbnd  38124  heibor  38156  unichnidl  38366  pexmidlem8N  40437  sn-0tie0  42910  nna4b4nsq  43107  elrfi  43140  fnwe2lem2  43497  hbtlem5  43574  rexlimdvaacbv  44650  rexlimddvcbvw  44651  relpfrlem  45398  liminfval2  46214  2zrngamgm  48733