Theorem rexlimiv 3243

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

Syntax hints:   → wi 4   ∈ wcel 2081  ∀wral 3105  ∃wrex 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-ral 3110  df-rex 3111

This theorem is referenced by:  rexlimiva  3244  rexlimivw  3245  rexlimdv  3246  rexlimivv  3255  clel5OLD  3596  rexn0  4368  issn  4670  uniss2  4777  disjiun  4950  reuop  6019  ssimaex  6615  ordzsl  7416  onzsl  7417  mpoexw  7632  tfrlem8  7872  nneob  8129  ecoptocl  8237  elixpsn  8349  ixpsnf1o  8350  php  8548  php3  8550  ssfi  8584  findcard  8603  findcard2  8604  ordunifi  8614  fiint  8641  en3lp  8923  inf0  8930  inf3lemd  8936  inf3lem6  8942  noinfep  8969  cantnfvalf  8974  trcl  9016  bndrank  9116  rankc2  9146  tcrank  9159  ficardom  9236  ac10ct  9306  isinfcard  9364  alephfp  9380  dfac5lem4  9398  dfac2b  9402  ackbij2  9511  fin23lem16  9603  fin23lem29  9609  fin17  9662  fin1a2lem6  9673  itunitc  9689  hsmexlem9  9693  axdc3lem2  9719  axdc3lem4  9721  axcclem  9725  zorn2lem7  9770  wunr1om  9987  tskr1om  10035  grothomex  10097  prnmadd  10265  ltaprlem  10312  mulgt0sr  10373  0cnALT2  10722  renegcli  10795  peano2nn  11498  bndndx  11744  uzn0  12109  ublbneg  12182  om2uzrani  13170  uzrdgfni  13176  exprelprel  13693  rtrclreclem3  14253  rtrclind  14258  rexanuz2  14543  caurcvg  14867  caucvg  14869  infcvgaux1i  15045  vdwlem6  16151  dfgrp2e  17887  efgrelexlemb  18603  cygth  20400  iscldtop  21387  opnneiid  21418  pnfnei  21512  mnfnei  21513  discmp  21690  cmpsublem  21691  cmpfi  21700  2ndcredom  21742  2ndc1stc  21743  2ndcdisj  21748  kgenidm  21839  methaus  22813  xrtgioo  23097  caun0  23567  ovolmge0  23761  itg2lcl  24011  aannenlem2  24601  aannenlem3  24602  aaliou2  24612  leibpilem1OLD  25200  2lgslem1b  25650  2sqlem2  25676  ostth  25897  midwwlks2s3  27418  3cyclfrgrrn1  27756  3cyclfrgrrn  27757  h1de2ctlem  29023  h1de2ci  29024  spansni  29025  spanunsni  29047  riesz3i  29530  adjbd1o  29553  rnbra  29575  pjnmopi  29616  dfpjop  29650  atom1d  29821  cvexchlem  29836  cdj1i  29901  cdj3lem1  29902  hasheuni  30961  cvmlift2lem12  32169  satfrnmapom  32225  sat1el2xp  32234  fmla1  32242  gonar  32250  goalr  32252  fmla0disjsuc  32253  mrsubccat  32373  msrid  32400  elmthm  32431  untint  32546  dfon2lem3  32638  dfon2lem7  32642  dfrdg2  32649  trpred0  32684  nodmon  32766  sltval2  32772  bdayfo  32791  finminlem  33275  fneint  33305  ptrecube  34423  poimirlem26  34449  poimirlem27  34450  poimirlem29  34452  poimirlem30  34453  zerdivemp1x  34757  dochsnnz  38117  ismrc  38783  eldiophb  38839  eldioph4b  38893  dfacbasgrp  39193  dfsucon  39374  subsaliuncllem  42182  icoresmbl  42367  sprsymrelfvlem  43134  sprsymrelf1lem  43135  prmdvdsfmtnof1lem2  43229  uspgropssxp  43501