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

Theorem rexlimiv 3173
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 3068 . 2 𝑥𝐴 (𝜑𝜓)
3 r19.23v 3169 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
42, 3mpbi 221 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wral 3054  wrex 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3059  df-rex 3060
This theorem is referenced by:  rexlimiva  3174  rexlimivw  3175  rexlimdv  3176  rexlimivv  3182  clel5  3496  rexn0  4232  issn  4514  uniss2  4627  disjiun  4796  elresOLD  5610  ssimaex  6451  ordzsl  7242  onzsl  7243  tfrlem8  7683  nneob  7936  ecoptocl  8039  elixpsn  8151  ixpsnf1o  8152  php  8350  php3  8352  ssfi  8386  findcard  8405  findcard2  8406  ordunifi  8416  fiint  8443  en3lp  8723  inf0  8732  inf3lemd  8738  inf3lem6  8744  noinfep  8771  cantnfvalf  8776  trcl  8818  bndrank  8918  rankc2  8948  tcrank  8961  ficardom  9037  ac10ct  9107  isinfcard  9165  alephfp  9181  dfac5lem4  9199  dfac2b  9203  dfac2OLD  9205  ackbij2  9317  fin23lem16  9409  fin23lem29  9415  fin17  9468  fin1a2lem6  9479  itunitc  9495  hsmexlem9  9499  axdc3lem2  9525  axdc3lem4  9527  axcclem  9531  zorn2lem7  9576  wunr1om  9793  tskr1om  9841  grothomex  9903  prnmadd  10071  ltaprlem  10118  mulgt0sr  10178  0reOLD  10295  0cnALT  10523  renegcli  10595  peano2nn  11287  bndndx  11536  uzn0  11901  ublbneg  11973  om2uzrani  12958  uzrdgfni  12964  exprelprel  13471  rtrclreclem3  14086  rtrclind  14091  rexanuz2  14375  caurcvg  14693  caucvg  14695  infcvgaux1i  14874  vdwlem6  15970  dfgrp2e  17716  efgrelexlemb  18428  cygth  20191  iscldtop  21178  opnneiid  21209  pnfnei  21303  mnfnei  21304  discmp  21480  cmpsublem  21481  cmpfi  21490  2ndcredom  21532  2ndc1stc  21533  2ndcdisj  21538  kgenidm  21629  methaus  22603  xrtgioo  22887  caun0  23357  ovolmge0  23534  itg2lcl  23784  aannenlem2  24374  aannenlem3  24375  aaliou2  24385  leibpilem1  24957  2lgslem1b  25407  2sqlem2  25433  ostth  25618  midwwlks2s3  27154  3cyclfrgrrn1  27522  3cyclfrgrrn  27523  h1de2ctlem  28804  h1de2ci  28805  spansni  28806  spanunsni  28828  riesz3i  29311  adjbd1o  29334  rnbra  29356  pjnmopi  29397  dfpjop  29431  atom1d  29602  cvexchlem  29617  cdj1i  29682  cdj3lem1  29683  hasheuni  30528  cvmlift2lem12  31675  mrsubccat  31794  msrid  31821  elmthm  31852  untint  31966  dfon2lem3  32064  dfon2lem7  32068  dfrdg2  32075  trpred0  32110  nodmon  32178  sltval2  32184  bdayfo  32203  finminlem  32687  fneint  32717  cnfinltrel  33606  ptrecube  33765  poimirlem26  33791  poimirlem27  33792  poimirlem29  33794  poimirlem30  33795  zerdivemp1x  34100  dochsnnz  37338  ismrc  37874  eldiophb  37930  eldioph4b  37985  dfacbasgrp  38287  subsaliuncllem  41144  icoresmbl  41329  prmdvdsfmtnof1lem2  42105  sprsymrelfvlem  42341  sprsymrelf1lem  42342  uspgropssxp  42353
  Copyright terms: Public domain W3C validator