Theorem rexlimiv 3009

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  rexlimiva  3010  rexlimivw  3011  rexlimdv  3012  rexlimivv  3018  rexn0  4026  uniss2  4406  disjiun  4573  elres  5355  ssimaex  6173  ordzsl  6937  onzsl  6938  tfrlem8  7367  nneob  7619  ecoptocl  7724  mapsn  7785  elixpsn  7833  ixpsnf1o  7834  php  8029  php3  8031  ssfi  8065  findcard  8084  findcard2  8085  ordunifi  8095  fiint  8122  en3lp  8396  inf0  8401  inf3lemd  8407  inf3lem6  8413  noinfep  8440  cantnfvalf  8445  trcl  8487  bndrank  8587  rankc2  8617  tcrank  8630  ficardom  8670  ac10ct  8740  isinfcard  8798  alephfp  8814  dfac5lem4  8832  dfac2  8836  ackbij2  8948  fin23lem16  9040  fin23lem29  9046  fin17  9099  fin1a2lem6  9110  itunitc  9126  hsmexlem9  9130  axdc3lem2  9156  axdc3lem4  9158  axcclem  9162  zorn2lem7  9207  wunr1om  9420  tskr1om  9468  grothomex  9530  prnmadd  9698  ltaprlem  9745  mulgt0sr  9805  0re  9919  0cnALT  10149  renegcli  10221  peano2nn  10909  bndndx  11168  uzn0  11579  ublbneg  11649  om2uzrani  12613  uzrdgfni  12619  exprelprel  13126  rtrclreclem3  13648  rtrclind  13653  rexanuz2  13937  caurcvg  14255  caucvg  14257  infcvgaux1i  14428  vdwlem6  15528  dfgrp2e  17271  efgrelexlemb  17986  cygth  19739  iscldtop  20709  opnneiid  20740  pnfnei  20834  mnfnei  20835  discmp  21011  cmpsublem  21012  cmpfi  21021  2ndcredom  21063  2ndc1stc  21064  2ndcdisj  21069  kgenidm  21160  methaus  22135  xrtgioo  22417  caun0  22887  ovolmge0  23052  itg2lcl  23300  aannenlem2  23888  aannenlem3  23889  aaliou2  23899  leibpilem1  24467  2lgslem1b  24917  2sqlem2  24943  ostth  25128  eupatrl  26495  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  h1de2ctlem  27798  h1de2ci  27799  spansni  27800  spanunsni  27822  riesz3i  28305  adjbd1o  28328  rnbra  28350  pjnmopi  28391  dfpjop  28425  atom1d  28596  cvexchlem  28611  cdj1i  28676  cdj3lem1  28677  hasheuni  29474  cvmlift2lem12  30550  mrsubccat  30669  msrid  30696  elmthm  30727  untint  30843  dfon2lem3  30934  dfon2lem7  30938  dfrdg2  30945  trpred0  30980  nodmon  31047  sltval2  31053  bdayfo  31074  nofulllem5  31105  finminlem  31482  fneint  31513  ptrecube  32579  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  zerdivemp1x  32916  dochsnnz  35757  ismrc  36282  eldiophb  36338  eldioph4b  36393  dfacbasgrp  36697  subsaliuncllem  39251  icoresmbl  39433  prmdvdsfmtnof1lem2  40035  clel5  40303  3cyclfrgrrn1  41455  3cyclfrgrrn  41456