Theorem rexlimdvaa 3155

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  rexlimddv  3160  tz7.7  6390  isofrlem  7340  nnawordex  8641  oaabs2  8652  fiin  9421  marypha1lem  9432  wemaplem3  9547  cantnflt  9671  fseqenlem2  10024  cardaleph  10088  coftr  10272  fin23lem26  10324  fin1a2lem13  10411  fpwwe2  10642  r1wunlim  10736  wunex2  10737  inttsk  10773  grur1  10819  inaprc  10835  receu  11864  zsupss  12926  xralrple  13189  rexanuz  15297  limsupval2  15429  caucvgb  15631  fsumiun  15772  rpnnen2lem12  16173  dvdsval2  16205  prmind2  16627  prmdvdsncoprmbd  16668  pcprmpw2  16820  pockthg  16844  prmreclem5  16858  vdwlem6  16924  vdwlem10  16928  sscpwex  17767  drsdirfi  18263  psgnunilem3  19406  sylow3lem2  19538  efgsfo  19649  lt6abl  19805  ghmcyg  19806  ablsimpgfind  20022  unitgrp  20275  irredrmul  20319  drngnidl  21004  znunit  21339  tgcl  22693  neiint  22829  restopnb  22900  ordtrest2lem  22928  pnfnei  22945  mnfnei  22946  iscnp4  22988  haust1  23077  ordthauslem  23108  tgcmp  23126  t1connperf  23161  2ndc1stc  23176  2ndcdisj  23181  islly2  23209  nllyrest  23211  reftr  23239  comppfsc  23257  ptbasfi  23306  ptcnp  23347  xkococnlem  23384  tgqtop  23437  fbssfi  23562  fgabs  23604  neifil  23605  trfil2  23612  elfm2  23673  elfm3  23675  rnelfmlem  23677  fmfnfmlem4  23682  flffbas  23720  fclsfnflim  23752  ptcmplem4  23780  tsmsxp  23880  blssexps  24153  blssex  24154  icccmplem3  24561  cnheibor  24702  pi1blem  24787  iscfil3  25022  iscmet3lem2  25041  metsscmetcld  25064  ovolicc2  25272  nulmbl2  25286  volsup  25306  dyadmbllem  25349  itg2const2  25492  bddmulibl  25589  bddiblnc  25592  limcflf  25631  itgsubst  25802  ulmdvlem3  26151  xrlimcnp  26710  amgm  26732  dchrptlem2  27005  lgsne0  27075  lgsqr  27091  lgsquadlem1  27120  dchrvmasumif  27243  rpvmasum2  27252  dchrisum0re  27253  dchrisum0lem3  27259  dchrisum0  27260  dchrmusum  27264  dchrvmasum  27265  chpdifbnd  27295  pntrlog2bnd  27324  pntibndlem3  27332  pntibnd  27333  pntleml  27351  ostth  27379  nosupno  27443  nosupbnd1lem1  27448  nosupbnd2  27456  noinfno  27458  noinfbnd1lem1  27463  noinfbnd2  27471  scutbdaybnd2  27555  oldlim  27619  oldbdayim  27621  sleadd1  27712  norecdiv  27878  precsexlem11  27903  brbtwn2  28431  colinearalg  28436  nbumgrvtx  28871  cusgrfilem1  28980  nmobndi  30296  spansneleq  31091  ofrn2  32133  xreceu  32356  ordtrest2NEWlem  33201  dya2iocnei  33580  connpconn  34525  cvmsss2  34564  cvmlift2lem10  34602  cvmlift3lem2  34610  outsidele  35409  neibastop1  35548  neibastop2lem  35549  matunitlindflem1  36788  mblfinlem1  36829  mblfinlem3  36831  mblfinlem4  36832  ismblfin  36833  cnambfre  36840  itg2addnclem  36843  itg2addnclem3  36845  ftc1anclem7  36871  ftc1anc  36873  fdc  36917  sstotbnd2  36946  sstotbnd  36947  isbndx  36954  ssbnd  36960  totbndbnd  36961  heibor  36993  unichnidl  37203  pexmidlem8N  39152  sn-0tie0  41615  nna4b4nsq  41705  elrfi  41735  fnwe2lem2  42096  hbtlem5  42173  rexlimdvaacbv  43260  rexlimddvcbvw  43261  liminfval2  44783  2zrngamgm  46926