Theorem rexlimiv 3209

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexlimiva  3210  rexlimivw  3211  rexlimdv  3212  rexlimivv  3221  rexn0OLD  4445  issn  4763  uniss2  4874  disjiun  5061  reuop  6196  ssimaex  6853  ordzsl  7692  onzsl  7693  mpoexw  7919  fsplitfpar  7959  tfrlem8  8215  nneob  8486  ecoptocl  8596  elixpsn  8725  ixpsnf1o  8726  findcard  8946  findcard2  8947  ssfiALT  8957  php  8993  php3  8995  phpOLD  9005  php3OLD  9007  findcard2OLD  9056  ordunifi  9064  fiint  9091  en3lp  9372  inf0  9379  inf3lemd  9385  inf3lem6  9391  noinfep  9418  cantnfvalf  9423  dmttrcl  9479  rnttrcl  9480  ttrclselem1  9483  trcl  9486  bndrank  9599  rankc2  9629  tcrank  9642  ficardom  9719  ac10ct  9790  isinfcard  9848  alephfp  9864  dfac5lem4  9882  dfac2b  9886  ackbij2  9999  fin23lem16  10091  fin23lem29  10097  fin17  10150  fin1a2lem6  10161  itunitc  10177  hsmexlem9  10181  axdc3lem2  10207  axdc3lem4  10209  axcclem  10213  zorn2lem7  10258  wunr1om  10475  tskr1om  10523  grothomex  10585  prnmadd  10753  ltaprlem  10800  mulgt0sr  10861  0cnALT2  11210  renegcli  11282  peano2nn  11985  bndndx  12232  uzn0  12599  ublbneg  12673  om2uzrani  13672  uzrdgfni  13678  exprelprel  14203  rtrclreclem3  14771  rtrclind  14776  rexanuz2  15061  caurcvg  15388  caucvg  15390  infcvgaux1i  15569  vdwlem6  16687  dfgrp2e  18605  efgrelexlemb  19356  cygth  20779  psgnghm  20785  iscldtop  22246  opnneiid  22277  pnfnei  22371  mnfnei  22372  discmp  22549  cmpsublem  22550  cmpfi  22559  2ndcredom  22601  2ndc1stc  22602  2ndcdisj  22607  kgenidm  22698  methaus  23676  xrtgioo  23969  caun0  24445  ovolmge0  24641  itg2lcl  24892  aannenlem2  25489  aannenlem3  25490  aaliou2  25500  2lgslem1b  26540  2sqlem2  26566  ostth  26787  midwwlks2s3  28317  3cyclfrgrrn1  28649  3cyclfrgrrn  28650  h1de2ctlem  29917  h1de2ci  29918  spansni  29919  spanunsni  29941  riesz3i  30424  adjbd1o  30447  rnbra  30469  pjnmopi  30510  dfpjop  30544  atom1d  30715  cvexchlem  30730  cdj1i  30795  cdj3lem1  30796  hasheuni  32053  cvmlift2lem12  33276  satfrnmapom  33332  sat1el2xp  33341  fmla1  33349  gonar  33357  goalr  33359  fmla0disjsuc  33360  mrsubccat  33480  msrid  33507  elmthm  33538  untint  33653  nnuni  33692  dfon2lem3  33761  dfon2lem7  33765  dfrdg2  33771  nodmon  33853  sltval2  33859  bdayfo  33880  madef  34040  finminlem  34507  fneint  34537  ptrecube  35777  poimirlem26  35803  poimirlem27  35804  poimirlem29  35806  poimirlem30  35807  zerdivemp1x  36105  dochsnnz  39464  ismrc  40523  eldiophb  40579  eldioph4b  40633  dfacbasgrp  40933  dfsucon  41130  subsaliuncllem  43896  icoresmbl  44081  elsetpreimafvssdm  44838  sprsymrelfvlem  44942  sprsymrelf1lem  44943  prmdvdsfmtnof1lem2  45037  uspgropssxp  45306  0aryfvalel  45980