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

Theorem rexlimiv 2784
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
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 nfv 1626 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2783 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  rexlimiva  2785  rexlimivw  2786  rexlimivv  2795  r19.36av  2816  r19.44av  2824  r19.45av  2825  rexn0  3690  uniss2  4006  disjiun  4162  ordzsl  4784  onzsl  4785  elres  5140  ssimaex  5747  tfrlem8  6604  nneob  6854  ecoptocl  6953  mapsn  7014  elixpsn  7060  ixpsnf1o  7061  php  7250  php3  7252  ssfi  7288  findcard  7306  findcard2  7307  ordunifi  7316  fiint  7342  inf0  7532  inf3lemd  7538  inf3lem6  7544  noinfep  7570  cantnfvalf  7576  trcl  7620  en3lp  7628  bndrank  7723  rankc2  7753  tcrank  7764  ficardom  7804  ac10ct  7871  isinfcard  7929  alephfp  7945  dfac5lem4  7963  dfac2  7967  ackbij2  8079  fin23lem16  8171  fin23lem29  8177  fin17  8230  fin1a2lem6  8241  itunitc  8257  hsmexlem9  8261  axdc3lem2  8287  axdc3lem4  8289  axcclem  8293  zorn2lem7  8338  wunr1om  8550  tskr1om  8598  grothomex  8660  prnmadd  8830  ltaprlem  8877  mulgt0sr  8936  0re  9047  0cnALT  9251  renegcli  9318  infmrcl  9943  peano2nn  9968  bndndx  10176  uzn0  10457  ublbneg  10516  om2uzrani  11247  uzrdgfni  11253  rexanuz2  12108  caurcvg  12425  caucvg  12427  infcvgaux1i  12591  vdwlem6  13309  efgrelexlemb  15337  cygth  16807  iscldtop  17114  opnneiid  17145  pnfnei  17238  mnfnei  17239  discmp  17415  cmpsublem  17416  cmpfi  17425  2ndcredom  17466  2ndc1stc  17467  2ndcdisj  17472  kgenidm  17532  methaus  18503  xrtgioo  18790  caun0  19187  ovolmge0  19326  itg2lcl  19572  aannenlem2  20199  aannenlem3  20200  aaliou2  20210  leibpilem1  20733  2sqlem2  21101  ostth  21286  eupatrl  21643  zerdivemp1  21975  rngoridfz  21976  h1de2ctlem  23010  h1de2ci  23011  spansni  23012  spanunsni  23034  riesz3i  23518  adjbd1o  23541  rnbra  23563  pjnmopi  23604  dfpjop  23638  atom1d  23809  cvexchlem  23824  cdj1i  23889  cdj3lem1  23890  hasheuni  24428  cvmlift2lem12  24954  ghomgrpilem2  25050  rtrclreclem.trans  25099  rtrclind  25102  untint  25114  dfon2lem3  25355  dfon2lem7  25359  dfrdg2  25366  trpred0  25453  nodmon  25518  sltval2  25524  bdayfo  25543  nofulllem5  25574  finminlem  26211  fneint  26247  zerdivemp1x  26461  ismrc  26645  eldiophb  26705  eldioph4b  26762  dfacbasgrp  27141  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  dochsnnz  31933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator