Theorem rexlimdvaa 3248

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081  ∃wrex 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110  df-rex 3111

This theorem is referenced by:  rexlimddv  3254  tz7.7  6092  isofrlem  6956  nnawordex  8113  oaabs2  8122  fiin  8732  marypha1lem  8743  wemaplem3  8858  cantnflt  8981  fseqenlem2  9297  cardaleph  9361  coftr  9541  fin23lem26  9593  fin1a2lem13  9680  fpwwe2  9911  r1wunlim  10005  wunex2  10006  inttsk  10042  grur1  10088  inaprc  10104  receu  11133  zsupss  12186  xralrple  12448  rexanuz  14539  limsupval2  14671  caucvgb  14870  fsumiun  15009  rpnnen2lem12  15411  dvdsval2  15443  prmind2  15858  pcprmpw2  16047  pockthg  16071  prmreclem5  16085  vdwlem6  16151  vdwlem10  16155  sscpwex  16914  drsdirfi  17377  psgnunilem3  18355  sylow3lem2  18483  efgsfo  18592  lt6abl  18736  ghmcyg  18737  unitgrp  19107  irredrmul  19147  drngnidl  19691  znunit  20392  tgcl  21261  neiint  21396  restopnb  21467  ordtrest2lem  21495  pnfnei  21512  mnfnei  21513  iscnp4  21555  haust1  21644  ordthauslem  21675  tgcmp  21693  t1connperf  21728  2ndc1stc  21743  2ndcdisj  21748  islly2  21776  nllyrest  21778  reftr  21806  comppfsc  21824  ptbasfi  21873  ptcnp  21914  xkococnlem  21951  tgqtop  22004  fbssfi  22129  fgabs  22171  neifil  22172  trfil2  22179  elfm2  22240  elfm3  22242  rnelfmlem  22244  fmfnfmlem4  22249  flffbas  22287  fclsfnflim  22319  ptcmplem4  22347  tsmsxp  22446  blssexps  22719  blssex  22720  icccmplem3  23115  cnheibor  23242  pi1blem  23326  iscfil3  23559  iscmet3lem2  23578  metsscmetcld  23601  ovolicc2  23806  nulmbl2  23820  volsup  23840  dyadmbllem  23883  itg2const2  24025  bddmulibl  24122  limcflf  24162  itgsubst  24329  ulmdvlem3  24673  xrlimcnp  25228  amgm  25250  dchrptlem2  25523  lgsne0  25593  lgsqr  25609  lgsquadlem1  25638  dchrvmasumif  25761  rpvmasum2  25770  dchrisum0re  25771  dchrisum0lem3  25777  dchrisum0  25778  dchrmusum  25782  dchrvmasum  25783  chpdifbnd  25813  pntrlog2bnd  25842  pntibndlem3  25850  pntibnd  25851  pntleml  25869  ostth  25897  brbtwn2  26374  colinearalg  26379  nbumgrvtx  26811  cusgrfilem1  26920  nmobndi  28243  spansneleq  29038  ofrn2  30077  xreceu  30282  ordtrest2NEWlem  30782  dya2iocnei  31157  connpconn  32090  cvmsss2  32129  cvmlift2lem10  32167  cvmlift3lem2  32175  nosupno  32812  nosupbnd1lem1  32817  nosupbnd2  32825  scutbdaybnd  32884  outsidele  33202  neibastop1  33316  neibastop2lem  33317  matunitlindflem1  34419  mblfinlem1  34460  mblfinlem3  34462  mblfinlem4  34463  ismblfin  34464  cnambfre  34471  itg2addnclem  34474  itg2addnclem3  34476  bddiblnc  34493  ftc1anclem7  34504  ftc1anc  34506  fdc  34552  sstotbnd2  34584  sstotbnd  34585  isbndx  34592  ssbnd  34598  totbndbnd  34599  heibor  34631  unichnidl  34841  pexmidlem8N  36644  elrfi  38776  fnwe2lem2  39136  hbtlem5  39213  rexlimdvaacbv  40046  ablsimpgfind  40167  liminfval2  41591  2zrngamgm  43688