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

Theorem rexlimiv 3175
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 3071 . 2 𝑥𝐴 (𝜑𝜓)
3 r19.23v 3171 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
42, 3mpbi 220 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wral 3061  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  rexlimiva  3176  rexlimivw  3177  rexlimdv  3178  rexlimivv  3184  clel5  3494  rexn0  4215  issn  4496  uniss2  4606  disjiun  4774  elres  5576  ssimaex  6405  ordzsl  7192  onzsl  7193  tfrlem8  7633  nneob  7886  ecoptocl  7989  elixpsn  8101  ixpsnf1o  8102  php  8300  php3  8302  ssfi  8336  findcard  8355  findcard2  8356  ordunifi  8366  fiint  8393  en3lp  8673  inf0  8682  inf3lemd  8688  inf3lem6  8694  noinfep  8721  cantnfvalf  8726  trcl  8768  bndrank  8868  rankc2  8898  tcrank  8911  ficardom  8987  ac10ct  9057  isinfcard  9115  alephfp  9131  dfac5lem4  9149  dfac2b  9153  dfac2OLD  9155  ackbij2  9267  fin23lem16  9359  fin23lem29  9365  fin17  9418  fin1a2lem6  9429  itunitc  9445  hsmexlem9  9449  axdc3lem2  9475  axdc3lem4  9477  axcclem  9481  zorn2lem7  9526  wunr1om  9743  tskr1om  9791  grothomex  9853  prnmadd  10021  ltaprlem  10068  mulgt0sr  10128  0re  10242  0cnALT  10472  renegcli  10544  peano2nn  11234  bndndx  11493  uzn0  11904  ublbneg  11976  om2uzrani  12959  uzrdgfni  12965  exprelprel  13473  rtrclreclem3  14008  rtrclind  14013  rexanuz2  14297  caurcvg  14615  caucvg  14617  infcvgaux1i  14796  vdwlem6  15897  dfgrp2e  17656  efgrelexlemb  18370  cygth  20135  iscldtop  21120  opnneiid  21151  pnfnei  21245  mnfnei  21246  discmp  21422  cmpsublem  21423  cmpfi  21432  2ndcredom  21474  2ndc1stc  21475  2ndcdisj  21480  kgenidm  21571  methaus  22545  xrtgioo  22829  caun0  23298  ovolmge0  23465  itg2lcl  23714  aannenlem2  24304  aannenlem3  24305  aaliou2  24315  leibpilem1  24888  2lgslem1b  25338  2sqlem2  25364  ostth  25549  midwwlks2s3  27099  3cyclfrgrrn1  27467  3cyclfrgrrn  27468  h1de2ctlem  28754  h1de2ci  28755  spansni  28756  spanunsni  28778  riesz3i  29261  adjbd1o  29284  rnbra  29306  pjnmopi  29347  dfpjop  29381  atom1d  29552  cvexchlem  29567  cdj1i  29632  cdj3lem1  29633  hasheuni  30487  cvmlift2lem12  31634  mrsubccat  31753  msrid  31780  elmthm  31811  untint  31927  dfon2lem3  32026  dfon2lem7  32030  dfrdg2  32037  trpred0  32072  nodmon  32140  sltval2  32146  bdayfo  32165  finminlem  32649  fneint  32680  cnfinltrel  33578  ptrecube  33742  poimirlem26  33768  poimirlem27  33769  poimirlem29  33771  poimirlem30  33772  zerdivemp1x  34078  dochsnnz  37260  ismrc  37790  eldiophb  37846  eldioph4b  37901  dfacbasgrp  38204  subsaliuncllem  41092  icoresmbl  41277  prmdvdsfmtnof1lem2  42025  sprsymrelfvlem  42268  sprsymrelf1lem  42269  uspgropssxp  42280
  Copyright terms: Public domain W3C validator