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

Theorem rexlimiv 2873
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  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimiv  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimiv
StepHypRef Expression
1 rexlimiv.1 . . 3  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
21rgen 2747 . 2  |-  A. x  e.  A  ( ph  ->  ps )
3 r19.23v 2867 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
42, 3mpbi 212 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   A.wral 2737   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  rexlimiva  2875  rexlimivw  2876  rexlimdv  2877  rexlimivv  2884  r19.36v  2938  r19.44v  2947  r19.45v  2948  rexn0  3872  uniss2  4230  disjiun  4393  elres  5140  ssimaex  5930  ordzsl  6672  onzsl  6673  tfrlem8  7102  nneob  7353  ecoptocl  7453  mapsn  7513  elixpsn  7561  ixpsnf1o  7562  php  7756  php3  7758  ssfi  7792  findcard  7810  findcard2  7811  ordunifi  7821  fiint  7848  en3lp  8121  inf0  8126  inf3lemd  8132  inf3lem6  8138  noinfep  8165  cantnfvalf  8170  trcl  8212  bndrank  8312  rankc2  8342  tcrank  8355  ficardom  8395  ac10ct  8465  isinfcard  8523  alephfp  8539  dfac5lem4  8557  dfac2  8561  ackbij2  8673  fin23lem16  8765  fin23lem29  8771  fin17  8824  fin1a2lem6  8835  itunitc  8851  hsmexlem9  8855  axdc3lem2  8881  axdc3lem4  8883  axcclem  8887  zorn2lem7  8932  wunr1om  9144  tskr1om  9192  grothomex  9254  prnmadd  9422  ltaprlem  9469  mulgt0sr  9529  0re  9643  0cnALT  9864  renegcli  9935  infmrclOLD  10593  peano2nn  10621  bndndx  10868  uzn0  11174  ublbneg  11248  om2uzrani  12166  uzrdgfni  12172  exprelprel  12646  rtrclreclem3  13123  rtrclind  13128  rexanuz2  13412  caurcvg  13742  caurcvgOLD  13743  caucvg  13745  infcvgaux1i  13915  vdwlem6  14936  efgrelexlemb  17400  cygth  19142  iscldtop  20111  opnneiid  20142  pnfnei  20236  mnfnei  20237  discmp  20413  cmpsublem  20414  cmpfi  20423  2ndcredom  20465  2ndc1stc  20466  2ndcdisj  20471  kgenidm  20562  methaus  21535  xrtgioo  21824  caun0  22251  ovolmge0  22430  itg2lcl  22685  aannenlem2  23285  aannenlem3  23286  aaliou2  23296  leibpilem1  23866  2sqlem2  24292  ostth  24477  eupatrl  25696  3cyclfrgrarn1  25740  3cyclfrgrarn  25741  zerdivemp1  26162  rngoridfz  26163  h1de2ctlem  27208  h1de2ci  27209  spansni  27210  spanunsni  27232  riesz3i  27715  adjbd1o  27738  rnbra  27760  pjnmopi  27801  dfpjop  27835  atom1d  28006  cvexchlem  28021  cdj1i  28086  cdj3lem1  28087  hasheuni  28906  cvmlift2lem12  30037  mrsubccat  30156  msrid  30183  elmthm  30214  ghomgrpilem2  30304  untint  30339  dfon2lem3  30431  dfon2lem7  30435  dfrdg2  30442  trpred0  30477  nodmon  30537  sltval2  30543  bdayfo  30564  nofulllem5  30595  finminlem  30974  fneint  31004  ptrecube  31940  poimirlem26  31966  poimirlem27  31967  poimirlem29  31969  poimirlem30  31970  zerdivemp1x  32194  dochsnnz  35018  ismrc  35543  eldiophb  35599  eldioph4b  35654  dfacbasgrp  35967  icoresmbl  38365  clel5  38981
  Copyright terms: Public domain W3C validator