Theorem rexlimiv 3162

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

Hypothesis

Ref	Expression
rexlimiv.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
rexlimiv	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		rexlimiv.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imp 412	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3161	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  rexlimdv  3167  rexlimivv  3210  issn  4802  uniss2  4912  disjiun  5102  reuop  6301  ssimaex  6973  ordzsl  7850  onzsl  7851  mpoexw  8084  fsplitfpar  8122  tfrlem8  8380  nneob  8651  ecoptocl  8814  elixpsn  8944  ixpsnf1o  8945  findcard  9158  findcard2  9159  ssfiALT  9168  php  9201  php3  9203  ordunifi  9260  fiint  9296  en3lp  9593  inf0  9600  inf3lemd  9606  inf3lem6  9612  noinfep  9639  cantnfvalf  9644  dmttrcl  9700  rnttrcl  9701  ttrclselem1  9704  trcl  9707  bndrank  9823  rankc2  9853  tcrank  9866  ficardom  9966  ac10ct  10037  isinfcard  10095  alephfp  10111  dfac5lem4  10129  dfac2b  10133  ackbij2  10244  fin23lem16  10337  fin23lem29  10343  fin17  10396  fin1a2lem6  10407  itunitc  10423  hsmexlem9  10427  axdc3lem2  10453  axdc3lem4  10455  axcclem  10459  zorn2lem7  10504  wunr1om  10722  tskr1om  10770  grothomex  10832  prnmadd  11000  ltaprlem  11047  mulgt0sr  11108  0cnALT2  11464  renegcli  11537  peano2nn  12263  bndndx  12521  uzn0  12897  ublbneg  12975  om2uzrani  14008  uzrdgfni  14014  exprelprel  14547  rtrclreclem3  15123  rtrclind  15128  rexanuz2  15427  caurcvg  15754  caucvg  15756  infcvgaux1i  15937  vdwlem6  17071  dfgrp2e  19061  efgrelexlemb  19851  pzriprnglem5  21672  pzriprnglem6  21673  pzriprnglem12  21679  cygth  21758  psgnghm  21767  iscldtop  23289  opnneiid  23320  pnfnei  23414  mnfnei  23415  discmp  23592  cmpsublem  23593  cmpfi  23602  2ndcredom  23644  2ndc1stc  23645  2ndcdisj  23650  kgenidm  23741  methaus  24714  xrtgioo  25001  caun0  25477  ovolmge0  25673  itg2lcl  25923  aannenlem2  26529  aannenlem3  26530  aaliou2  26540  2lgslem1b  27593  2sqlem2  27619  ostth  27840  nodmon  27851  ltsval2  27857  bdayfo  27878  madef  28066  addsprop  28206  negsprop  28265  mulsprop  28360  elons2  28488  nnsge1  28573  onsfi  28586  dfnns2  28602  n0seo  28651  bdaypw2n0bnd  28694  remulscllem1  28730  midwwlks2s3  30338  3cyclfrgrrn1  30673  3cyclfrgrrn  30674  h1de2ctlem  31944  h1de2ci  31945  spansni  31946  spanunsni  31968  riesz3i  32451  adjbd1o  32474  rnbra  32496  pjnmopi  32537  dfpjop  32571  atom1d  32742  cvexchlem  32757  cdj1i  32822  cdj3lem1  32823  hasheuni  34506  cvmlift2lem12  35827  satfrnmapom  35883  sat1el2xp  35892  fmla1  35900  gonar  35908  goalr  35910  fmla0disjsuc  35911  mrsubccat  36031  msrid  36058  elmthm  36089  untint  36225  nnuni  36240  dfon2lem3  36296  dfon2lem7  36300  dfrdg2  36306  finminlem  36870  fneint  36900  ptrecube  38312  poimirlem26  38338  poimirlem27  38339  poimirlem29  38341  poimirlem30  38342  zerdivemp1x  38639  dochsnnz  42265  ismrc  43473  eldiophb  43529  eldioph4b  43579  dfacbasgrp  43876  dfsucon  44290  orbitcl  45707  subsaliuncllem  47112  icoresmbl  47298  elsetpreimafvssdm  48176  sprsymrelfvlem  48280  sprsymrelf1lem  48281  prmdvdsfmtnof1lem2  48378  isgrtri  48749  stgredgel  48763  stgr1  48767  uspgropssxp  48950  0aryfvalel  49455