Theorem rexlimdvaa 3162

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimddv  3167  tz7.7  6421  isofrlem  7376  nnawordex  8693  nnaordex2  8695  oaabs2  8705  fiin  9491  marypha1lem  9502  wemaplem3  9617  cantnflt  9741  fseqenlem2  10094  cardaleph  10158  coftr  10342  fin23lem26  10394  fin1a2lem13  10481  fpwwe2  10712  r1wunlim  10806  wunex2  10807  inttsk  10843  grur1  10889  inaprc  10905  receu  11935  zsupss  13002  xralrple  13267  rexanuz  15394  limsupval2  15526  caucvgb  15728  fsumiun  15869  rpnnen2lem12  16273  dvdsval2  16305  prmind2  16732  prmdvdsncoprmbd  16774  pcprmpw2  16929  pockthg  16953  prmreclem5  16967  vdwlem6  17033  vdwlem10  17037  sscpwex  17876  drsdirfi  18375  psgnunilem3  19538  sylow3lem2  19670  efgsfo  19781  lt6abl  19937  ghmcyg  19938  ablsimpgfind  20154  unitgrp  20409  irredrmul  20453  drngnidl  21276  znunit  21605  tgcl  22997  neiint  23133  restopnb  23204  ordtrest2lem  23232  pnfnei  23249  mnfnei  23250  iscnp4  23292  haust1  23381  ordthauslem  23412  tgcmp  23430  t1connperf  23465  2ndc1stc  23480  2ndcdisj  23485  islly2  23513  nllyrest  23515  reftr  23543  comppfsc  23561  ptbasfi  23610  ptcnp  23651  xkococnlem  23688  tgqtop  23741  fbssfi  23866  fgabs  23908  neifil  23909  trfil2  23916  elfm2  23977  elfm3  23979  rnelfmlem  23981  fmfnfmlem4  23986  flffbas  24024  fclsfnflim  24056  ptcmplem4  24084  tsmsxp  24184  blssexps  24457  blssex  24458  icccmplem3  24865  cnheibor  25006  pi1blem  25091  iscfil3  25326  iscmet3lem2  25345  metsscmetcld  25368  ovolicc2  25576  nulmbl2  25590  volsup  25610  dyadmbllem  25653  itg2const2  25796  bddmulibl  25894  bddiblnc  25897  limcflf  25936  itgsubst  26110  ulmdvlem3  26463  xrlimcnp  27029  amgm  27052  dchrptlem2  27327  lgsne0  27397  lgsqr  27413  lgsquadlem1  27442  dchrvmasumif  27565  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem3  27581  dchrisum0  27582  dchrmusum  27586  dchrvmasum  27587  chpdifbnd  27617  pntrlog2bnd  27646  pntibndlem3  27654  pntibnd  27655  pntleml  27673  ostth  27701  nosupno  27766  nosupbnd1lem1  27771  nosupbnd2  27779  noinfno  27781  noinfbnd1lem1  27786  noinfbnd2  27794  scutbdaybnd2  27879  oldlim  27943  oldbdayim  27945  sleadd1  28040  norecdiv  28234  precsexlem11  28259  noseqrdgfn  28330  brbtwn2  28938  colinearalg  28943  nbumgrvtx  29381  cusgrfilem1  29491  nmobndi  30807  spansneleq  31602  ofrn2  32659  xreceu  32886  ordtrest2NEWlem  33868  dya2iocnei  34247  connpconn  35203  cvmsss2  35242  cvmlift2lem10  35280  cvmlift3lem2  35288  outsidele  36096  neibastop1  36325  neibastop2lem  36326  matunitlindflem1  37576  mblfinlem1  37617  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  cnambfre  37628  itg2addnclem  37631  itg2addnclem3  37633  ftc1anclem7  37659  ftc1anc  37661  fdc  37705  sstotbnd2  37734  sstotbnd  37735  isbndx  37742  ssbnd  37748  totbndbnd  37749  heibor  37781  unichnidl  37991  pexmidlem8N  39934  sn-0tie0  42415  nna4b4nsq  42615  elrfi  42650  fnwe2lem2  43008  hbtlem5  43085  rexlimdvaacbv  44167  rexlimddvcbvw  44168  liminfval2  45689  2zrngamgm  47968