Theorem rexlimdvaa 3167

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 461	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 3166	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimddv  3172  tz7.7  6388  isofrlem  7340  nnawordex  8624  nnaordex2  8626  oaabs2  8636  fiin  9383  marypha1lem  9394  wemaplem3  9511  cantnflt  9642  fseqenlem2  10010  cardaleph  10074  coftr  10258  fin23lem26  10310  fin1a2lem13  10397  fpwwe2  10629  r1wunlim  10723  wunex2  10724  inttsk  10760  grur1  10806  inaprc  10822  receu  11860  zsupss  12962  xralrple  13232  rexanuz  15399  limsupval2  15533  caucvgb  15733  fsumiun  15875  rpnnen2lem12  16282  dvdsval2  16314  prmind2  16744  prmdvdsncoprmbd  16787  pcprmpw2  16943  pockthg  16967  prmreclem5  16981  vdwlem6  17047  vdwlem10  17051  sscpwex  17873  drsdirfi  18362  psgnunilem3  19567  sylow3lem2  19699  efgsfo  19810  lt6abl  19966  ghmcyg  19967  ablsimpgfind  20183  unitgrp  20466  irredrmul  20510  unichnlidl  21343  drngnidl  21358  znunit  21694  tgcl  23107  neiint  23242  restopnb  23313  ordtrest2lem  23341  pnfnei  23358  mnfnei  23359  iscnp4  23401  haust1  23490  ordthauslem  23521  tgcmp  23539  t1connperf  23574  2ndc1stc  23589  2ndcdisj  23594  islly2  23622  nllyrest  23624  reftr  23652  comppfsc  23670  ptbasfi  23719  ptcnp  23760  xkococnlem  23797  tgqtop  23850  fbssfi  23975  fgabs  24017  neifil  24018  trfil2  24025  elfm2  24086  elfm3  24088  rnelfmlem  24090  fmfnfmlem4  24095  flffbas  24133  fclsfnflim  24165  ptcmplem4  24193  tsmsxp  24293  blssexps  24564  blssex  24565  icccmplem3  24963  cnheibor  25095  pi1blem  25179  iscfil3  25413  iscmet3lem2  25432  metsscmetcld  25455  ovolicc2  25662  nulmbl2  25676  volsup  25696  dyadmbllem  25739  itg2const2  25881  bddmulibl  25979  bddiblnc  25982  limcflf  26021  itgsubst  26189  ulmdvlem3  26546  xrlimcnp  27114  amgm  27136  dchrptlem2  27410  lgsne0  27480  lgsqr  27496  lgsquadlem1  27525  dchrvmasumif  27648  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lem3  27664  dchrisum0  27665  dchrmusum  27669  dchrvmasum  27670  chpdifbnd  27700  pntrlog2bnd  27729  pntibndlem3  27737  pntibnd  27738  pntleml  27756  ostth  27784  nosupno  27848  nosupbnd1lem1  27853  nosupbnd2  27861  noinfno  27863  noinfbnd1lem1  27868  noinfbnd2  27876  cutbdaybnd2  27970  oldlim  28061  oldbdayim  28063  leadds1  28163  norecdiv  28364  precsexlem11  28391  noseqrdgfn  28480  pw2recs  28612  z12sge0  28657  brbtwn2  29236  colinearalg  29241  nbumgrvtx  29677  cusgrfilem1  29786  nmobndi  31108  spansneleq  31903  ofrn2  32966  xreceu  33222  ordtrest2NEWlem  34293  dya2iocnei  34653  connpconn  35708  cvmsss2  35747  cvmlift2lem10  35785  cvmlift3lem2  35793  outsidele  36605  ltnadd  36676  neibastop1  36851  neibastop2lem  36852  ttctr  36985  dfttc2g  36998  dfttc4  37022  mh-inf3f1  37033  matunitlindflem1  38248  mblfinlem1  38289  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  cnambfre  38300  itg2addnclem  38303  itg2addnclem3  38305  ftc1anclem7  38331  ftc1anc  38333  fdc  38377  sstotbnd2  38406  sstotbnd  38407  isbndx  38414  ssbnd  38420  totbndbnd  38421  heibor  38453  unichnidl  38663  pexmidlem8N  40732  sn-0tie0  43206  nna4b4nsq  43375  elrfi  43408  fnwe2lem2  43761  hbtlem5  43838  rexlimdvaacbv  44912  rexlimddvcbvw  44913  relpfrlem  45645  liminfval2  46465  2zrngamgm  48993