Theorem rexlimiv 3208

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexlimiva  3209  rexlimivw  3210  rexlimdv  3211  rexlimivv  3220  rexn0OLD  4442  issn  4760  uniss2  4871  disjiun  5057  reuop  6185  ssimaex  6835  ordzsl  7667  onzsl  7668  mpoexw  7892  fsplitfpar  7930  tfrlem8  8186  nneob  8446  ecoptocl  8554  elixpsn  8683  ixpsnf1o  8684  php  8897  php3  8899  findcard  8908  findcard2  8909  ssfiALT  8919  findcard2OLD  8986  ordunifi  8994  fiint  9021  en3lp  9302  inf0  9309  inf3lemd  9315  inf3lem6  9321  noinfep  9348  cantnfvalf  9353  trpred0  9410  trcl  9417  bndrank  9530  rankc2  9560  tcrank  9573  ficardom  9650  ac10ct  9721  isinfcard  9779  alephfp  9795  dfac5lem4  9813  dfac2b  9817  ackbij2  9930  fin23lem16  10022  fin23lem29  10028  fin17  10081  fin1a2lem6  10092  itunitc  10108  hsmexlem9  10112  axdc3lem2  10138  axdc3lem4  10140  axcclem  10144  zorn2lem7  10189  wunr1om  10406  tskr1om  10454  grothomex  10516  prnmadd  10684  ltaprlem  10731  mulgt0sr  10792  0cnALT2  11140  renegcli  11212  peano2nn  11915  bndndx  12162  uzn0  12528  ublbneg  12602  om2uzrani  13600  uzrdgfni  13606  exprelprel  14131  rtrclreclem3  14699  rtrclind  14704  rexanuz2  14989  caurcvg  15316  caucvg  15318  infcvgaux1i  15497  vdwlem6  16615  dfgrp2e  18520  efgrelexlemb  19271  cygth  20691  psgnghm  20697  iscldtop  22154  opnneiid  22185  pnfnei  22279  mnfnei  22280  discmp  22457  cmpsublem  22458  cmpfi  22467  2ndcredom  22509  2ndc1stc  22510  2ndcdisj  22515  kgenidm  22606  methaus  23582  xrtgioo  23875  caun0  24350  ovolmge0  24546  itg2lcl  24797  aannenlem2  25394  aannenlem3  25395  aaliou2  25405  2lgslem1b  26445  2sqlem2  26471  ostth  26692  midwwlks2s3  28218  3cyclfrgrrn1  28550  3cyclfrgrrn  28551  h1de2ctlem  29818  h1de2ci  29819  spansni  29820  spanunsni  29842  riesz3i  30325  adjbd1o  30348  rnbra  30370  pjnmopi  30411  dfpjop  30445  atom1d  30616  cvexchlem  30631  cdj1i  30696  cdj3lem1  30697  hasheuni  31953  cvmlift2lem12  33176  satfrnmapom  33232  sat1el2xp  33241  fmla1  33249  gonar  33257  goalr  33259  fmla0disjsuc  33260  mrsubccat  33380  msrid  33407  elmthm  33438  untint  33553  nnuni  33595  dfon2lem3  33667  dfon2lem7  33671  dfrdg2  33677  dmttrcl  33707  rnttrcl  33708  ttrclselem1  33711  nodmon  33780  sltval2  33786  bdayfo  33807  madef  33967  finminlem  34434  fneint  34464  ptrecube  35704  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  zerdivemp1x  36032  dochsnnz  39391  ismrc  40439  eldiophb  40495  eldioph4b  40549  dfacbasgrp  40849  dfsucon  41028  subsaliuncllem  43786  icoresmbl  43971  elsetpreimafvssdm  44726  sprsymrelfvlem  44830  sprsymrelf1lem  44831  prmdvdsfmtnof1lem2  44925  uspgropssxp  45194  0aryfvalel  45868