Theorem rexlimiv 3282

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	rgen 3150	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		r19.23v 3281	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
4	2, 3	mpbi 232	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3140  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  rexlimiva  3283  rexlimivw  3284  rexlimdv  3285  rexlimivv  3294  clel5OLD  3660  rexn0  4456  issn  4765  uniss2  4873  disjiun  5055  reuop  6146  ssimaex  6750  ordzsl  7562  onzsl  7563  mpoexw  7778  fsplitfpar  7816  tfrlem8  8022  nneob  8281  ecoptocl  8389  elixpsn  8503  ixpsnf1o  8504  php  8703  php3  8705  ssfi  8740  findcard  8759  findcard2  8760  ordunifi  8770  fiint  8797  en3lp  9079  inf0  9086  inf3lemd  9092  inf3lem6  9098  noinfep  9125  cantnfvalf  9130  trcl  9172  bndrank  9272  rankc2  9302  tcrank  9315  ficardom  9392  ac10ct  9462  isinfcard  9520  alephfp  9536  dfac5lem4  9554  dfac2b  9558  ackbij2  9667  fin23lem16  9759  fin23lem29  9765  fin17  9818  fin1a2lem6  9829  itunitc  9845  hsmexlem9  9849  axdc3lem2  9875  axdc3lem4  9877  axcclem  9881  zorn2lem7  9926  wunr1om  10143  tskr1om  10191  grothomex  10253  prnmadd  10421  ltaprlem  10468  mulgt0sr  10529  0cnALT2  10877  renegcli  10949  peano2nn  11652  bndndx  11899  uzn0  12263  ublbneg  12336  om2uzrani  13323  uzrdgfni  13329  exprelprel  13850  rtrclreclem3  14421  rtrclind  14426  rexanuz2  14711  caurcvg  15035  caucvg  15037  infcvgaux1i  15214  vdwlem6  16324  dfgrp2e  18131  efgrelexlemb  18878  cygth  20720  psgnghm  20726  iscldtop  21705  opnneiid  21736  pnfnei  21830  mnfnei  21831  discmp  22008  cmpsublem  22009  cmpfi  22018  2ndcredom  22060  2ndc1stc  22061  2ndcdisj  22066  kgenidm  22157  methaus  23132  xrtgioo  23416  caun0  23886  ovolmge0  24080  itg2lcl  24330  aannenlem2  24920  aannenlem3  24921  aaliou2  24931  2lgslem1b  25970  2sqlem2  25996  ostth  26217  midwwlks2s3  27733  3cyclfrgrrn1  28066  3cyclfrgrrn  28067  h1de2ctlem  29334  h1de2ci  29335  spansni  29336  spanunsni  29358  riesz3i  29841  adjbd1o  29864  rnbra  29886  pjnmopi  29927  dfpjop  29961  atom1d  30132  cvexchlem  30147  cdj1i  30212  cdj3lem1  30213  hasheuni  31346  cvmlift2lem12  32563  satfrnmapom  32619  sat1el2xp  32628  fmla1  32636  gonar  32644  goalr  32646  fmla0disjsuc  32647  mrsubccat  32767  msrid  32794  elmthm  32825  untint  32940  dfon2lem3  33032  dfon2lem7  33036  dfrdg2  33042  trpred0  33077  nodmon  33159  sltval2  33165  bdayfo  33184  finminlem  33668  fneint  33698  ptrecube  34894  poimirlem26  34920  poimirlem27  34921  poimirlem29  34923  poimirlem30  34924  zerdivemp1x  35227  dochsnnz  38588  ismrc  39305  eldiophb  39361  eldioph4b  39415  dfacbasgrp  39715  dfsucon  39896  subsaliuncllem  42647  icoresmbl  42832  elsetpreimafvssdm  43553  sprsymrelfvlem  43659  sprsymrelf1lem  43660  prmdvdsfmtnof1lem2  43754  uspgropssxp  44026