Theorem rexlimiv 3199

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3061  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  rexlimiva  3200  rexlimivw  3201  rexlimdv  3202  rexlimivv  3211  rexn0OLD  4426  issn  4743  uniss2  4854  disjiun  5040  reuop  6156  ssimaex  6796  ordzsl  7624  onzsl  7625  mpoexw  7849  fsplitfpar  7887  tfrlem8  8120  nneob  8381  ecoptocl  8489  elixpsn  8618  ixpsnf1o  8619  php  8830  php3  8832  findcard  8841  findcard2  8842  ssfiALT  8852  findcard2OLD  8913  ordunifi  8921  fiint  8948  en3lp  9229  inf0  9236  inf3lemd  9242  inf3lem6  9248  noinfep  9275  cantnfvalf  9280  trpred0  9337  trcl  9344  bndrank  9457  rankc2  9487  tcrank  9500  ficardom  9577  ac10ct  9648  isinfcard  9706  alephfp  9722  dfac5lem4  9740  dfac2b  9744  ackbij2  9857  fin23lem16  9949  fin23lem29  9955  fin17  10008  fin1a2lem6  10019  itunitc  10035  hsmexlem9  10039  axdc3lem2  10065  axdc3lem4  10067  axcclem  10071  zorn2lem7  10116  wunr1om  10333  tskr1om  10381  grothomex  10443  prnmadd  10611  ltaprlem  10658  mulgt0sr  10719  0cnALT2  11067  renegcli  11139  peano2nn  11842  bndndx  12089  uzn0  12455  ublbneg  12529  om2uzrani  13525  uzrdgfni  13531  exprelprel  14055  rtrclreclem3  14623  rtrclind  14628  rexanuz2  14913  caurcvg  15240  caucvg  15242  infcvgaux1i  15421  vdwlem6  16539  dfgrp2e  18393  efgrelexlemb  19140  cygth  20536  psgnghm  20542  iscldtop  21992  opnneiid  22023  pnfnei  22117  mnfnei  22118  discmp  22295  cmpsublem  22296  cmpfi  22305  2ndcredom  22347  2ndc1stc  22348  2ndcdisj  22353  kgenidm  22444  methaus  23418  xrtgioo  23703  caun0  24178  ovolmge0  24374  itg2lcl  24625  aannenlem2  25222  aannenlem3  25223  aaliou2  25233  2lgslem1b  26273  2sqlem2  26299  ostth  26520  midwwlks2s3  28036  3cyclfrgrrn1  28368  3cyclfrgrrn  28369  h1de2ctlem  29636  h1de2ci  29637  spansni  29638  spanunsni  29660  riesz3i  30143  adjbd1o  30166  rnbra  30188  pjnmopi  30229  dfpjop  30263  atom1d  30434  cvexchlem  30449  cdj1i  30514  cdj3lem1  30515  hasheuni  31765  cvmlift2lem12  32989  satfrnmapom  33045  sat1el2xp  33054  fmla1  33062  gonar  33070  goalr  33072  fmla0disjsuc  33073  mrsubccat  33193  msrid  33220  elmthm  33251  untint  33366  nnuni  33408  dfon2lem3  33480  dfon2lem7  33484  dfrdg2  33490  dmttrcl  33520  rnttrcl  33521  nodmon  33590  sltval2  33596  bdayfo  33617  madef  33777  finminlem  34244  fneint  34274  ptrecube  35514  poimirlem26  35540  poimirlem27  35541  poimirlem29  35543  poimirlem30  35544  zerdivemp1x  35842  dochsnnz  39201  ismrc  40226  eldiophb  40282  eldioph4b  40336  dfacbasgrp  40636  dfsucon  40815  subsaliuncllem  43571  icoresmbl  43756  elsetpreimafvssdm  44511  sprsymrelfvlem  44615  sprsymrelf1lem  44616  prmdvdsfmtnof1lem2  44710  uspgropssxp  44979  0aryfvalel  45653