Theorem rexlimdvaa 3135

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexlimddv  3140  tz7.7  6339  isofrlem  7282  nnawordex  8560  nnaordex2  8562  oaabs2  8572  fiin  9315  marypha1lem  9326  wemaplem3  9443  cantnflt  9571  fseqenlem2  9925  cardaleph  9989  coftr  10173  fin23lem26  10225  fin1a2lem13  10312  fpwwe2  10543  r1wunlim  10637  wunex2  10638  inttsk  10674  grur1  10720  inaprc  10736  receu  11771  zsupss  12839  xralrple  13108  rexanuz  15257  limsupval2  15391  caucvgb  15591  fsumiun  15732  rpnnen2lem12  16138  dvdsval2  16170  prmind2  16600  prmdvdsncoprmbd  16642  pcprmpw2  16798  pockthg  16822  prmreclem5  16836  vdwlem6  16902  vdwlem10  16906  sscpwex  17726  drsdirfi  18215  psgnunilem3  19412  sylow3lem2  19544  efgsfo  19655  lt6abl  19811  ghmcyg  19812  ablsimpgfind  20028  unitgrp  20305  irredrmul  20349  drngnidl  21184  znunit  21504  tgcl  22887  neiint  23022  restopnb  23093  ordtrest2lem  23121  pnfnei  23138  mnfnei  23139  iscnp4  23181  haust1  23270  ordthauslem  23301  tgcmp  23319  t1connperf  23354  2ndc1stc  23369  2ndcdisj  23374  islly2  23402  nllyrest  23404  reftr  23432  comppfsc  23450  ptbasfi  23499  ptcnp  23540  xkococnlem  23577  tgqtop  23630  fbssfi  23755  fgabs  23797  neifil  23798  trfil2  23805  elfm2  23866  elfm3  23868  rnelfmlem  23870  fmfnfmlem4  23875  flffbas  23913  fclsfnflim  23945  ptcmplem4  23973  tsmsxp  24073  blssexps  24344  blssex  24345  icccmplem3  24743  cnheibor  24884  pi1blem  24969  iscfil3  25203  iscmet3lem2  25222  metsscmetcld  25245  ovolicc2  25453  nulmbl2  25467  volsup  25487  dyadmbllem  25530  itg2const2  25672  bddmulibl  25770  bddiblnc  25773  limcflf  25812  itgsubst  25986  ulmdvlem3  26341  xrlimcnp  26908  amgm  26931  dchrptlem2  27206  lgsne0  27276  lgsqr  27292  lgsquadlem1  27321  dchrvmasumif  27444  rpvmasum2  27453  dchrisum0re  27454  dchrisum0lem3  27460  dchrisum0  27461  dchrmusum  27465  dchrvmasum  27466  chpdifbnd  27496  pntrlog2bnd  27525  pntibndlem3  27533  pntibnd  27534  pntleml  27552  ostth  27580  nosupno  27645  nosupbnd1lem1  27650  nosupbnd2  27658  noinfno  27660  noinfbnd1lem1  27665  noinfbnd2  27673  scutbdaybnd2  27760  oldlim  27835  oldbdayim  27837  sleadd1  27935  norecdiv  28132  precsexlem11  28158  noseqrdgfn  28239  pw2recs  28364  zs12ge0  28396  brbtwn2  28887  colinearalg  28892  nbumgrvtx  29328  cusgrfilem1  29438  nmobndi  30759  spansneleq  31554  ofrn2  32626  xreceu  32911  ordtrest2NEWlem  33958  dya2iocnei  34318  connpconn  35302  cvmsss2  35341  cvmlift2lem10  35379  cvmlift3lem2  35387  outsidele  36199  neibastop1  36426  neibastop2lem  36427  matunitlindflem1  37679  mblfinlem1  37720  mblfinlem3  37722  mblfinlem4  37723  ismblfin  37724  cnambfre  37731  itg2addnclem  37734  itg2addnclem3  37736  ftc1anclem7  37762  ftc1anc  37764  fdc  37808  sstotbnd2  37837  sstotbnd  37838  isbndx  37845  ssbnd  37851  totbndbnd  37852  heibor  37884  unichnidl  38094  pexmidlem8N  40099  sn-0tie0  42572  nna4b4nsq  42781  elrfi  42814  fnwe2lem2  43171  hbtlem5  43248  rexlimdvaacbv  44325  rexlimddvcbvw  44326  relpfrlem  45073  liminfval2  45893  2zrngamgm  48372