MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimiv Structured version   Visualization version   GIF version

Theorem rexlimiv 3023
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
StepHypRef Expression
1 rexlimiv.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21rgen 2919 . 2 𝑥𝐴 (𝜑𝜓)
3 r19.23v 3019 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
42, 3mpbi 220 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wral 2909  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914  df-rex 2915
This theorem is referenced by:  rexlimiva  3024  rexlimivw  3025  rexlimdv  3026  rexlimivv  3032  clel5  3337  rexn0  4065  issn  4354  uniss2  4461  disjiun  4631  elres  5423  ssimaex  6250  ordzsl  7030  onzsl  7031  tfrlem8  7465  nneob  7717  ecoptocl  7822  mapsn  7884  elixpsn  7932  ixpsnf1o  7933  php  8129  php3  8131  ssfi  8165  findcard  8184  findcard2  8185  ordunifi  8195  fiint  8222  en3lp  8498  inf0  8503  inf3lemd  8509  inf3lem6  8515  noinfep  8542  cantnfvalf  8547  trcl  8589  bndrank  8689  rankc2  8719  tcrank  8732  ficardom  8772  ac10ct  8842  isinfcard  8900  alephfp  8916  dfac5lem4  8934  dfac2  8938  ackbij2  9050  fin23lem16  9142  fin23lem29  9148  fin17  9201  fin1a2lem6  9212  itunitc  9228  hsmexlem9  9232  axdc3lem2  9258  axdc3lem4  9260  axcclem  9264  zorn2lem7  9309  wunr1om  9526  tskr1om  9574  grothomex  9636  prnmadd  9804  ltaprlem  9851  mulgt0sr  9911  0re  10025  0cnALT  10255  renegcli  10327  peano2nn  11017  bndndx  11276  uzn0  11688  ublbneg  11758  om2uzrani  12734  uzrdgfni  12740  exprelprel  13254  rtrclreclem3  13781  rtrclind  13786  rexanuz2  14070  caurcvg  14388  caucvg  14390  infcvgaux1i  14570  vdwlem6  15671  dfgrp2e  17429  efgrelexlemb  18144  cygth  19901  iscldtop  20880  opnneiid  20911  pnfnei  21005  mnfnei  21006  discmp  21182  cmpsublem  21183  cmpfi  21192  2ndcredom  21234  2ndc1stc  21235  2ndcdisj  21240  kgenidm  21331  methaus  22306  xrtgioo  22590  caun0  23060  ovolmge0  23226  itg2lcl  23475  aannenlem2  24065  aannenlem3  24066  aaliou2  24076  leibpilem1  24648  2lgslem1b  25098  2sqlem2  25124  ostth  25309  midwwlks2s3  26841  3cyclfrgrrn1  27129  3cyclfrgrrn  27130  h1de2ctlem  28384  h1de2ci  28385  spansni  28386  spanunsni  28408  riesz3i  28891  adjbd1o  28914  rnbra  28936  pjnmopi  28977  dfpjop  29011  atom1d  29182  cvexchlem  29197  cdj1i  29262  cdj3lem1  29263  hasheuni  30121  cvmlift2lem12  31270  mrsubccat  31389  msrid  31416  elmthm  31447  untint  31563  dfon2lem3  31664  dfon2lem7  31668  dfrdg2  31675  trpred0  31710  nodmon  31777  sltval2  31783  bdayfo  31802  finminlem  32287  fneint  32318  ptrecube  33380  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem30  33410  zerdivemp1x  33717  dochsnnz  36558  ismrc  37083  eldiophb  37139  eldioph4b  37194  dfacbasgrp  37497  subsaliuncllem  40338  icoresmbl  40520  prmdvdsfmtnof1lem2  41262  sprsymrelfvlem  41505  sprsymrelf1lem  41506  uspgropssxp  41517
  Copyright terms: Public domain W3C validator