Theorem r19.21bi 2638

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
r19.21bi.1	|- ( ph -> A. x e. A ps )

Assertion

Ref	Expression
r19.21bi	|- ( ( ph /\ x e. A ) -> ps )

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . . 4 |- ( ph -> A. x e. A ps )
2		df-ral 2533	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 122	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1611	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 124	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1400   e. wcel 2209   A.wral 2528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1563

This theorem depends on definitions:  df-bi 117  df-ral 2533

This theorem is referenced by:  rspec2  2639  rspec3  2640  r19.21be  2641  frind  4492  wepo  4499  wetrep  4500  ordelord  4521  ralxfr2d  4605  rexxfr2d  4606  funfveu  5703  fvmptelcdm  5852  f1oresrab  5864  isoselem  6016  mpoexw  6439  disjxp1  6462  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  xpf1o  7134  fimax2gtrilemstep  7195  supisoti  7340  difinfsn  7430  exmidomni  7472  cc3  7624  prcdnql  7841  prcunqu  7842  prdisj  7849  caucvgsrlembound  8151  caucvgsrlemoffgt1  8156  exbtwnzlemex  10662  monoord2  10901  iseqf1olemqk  10922  seq3f1olemqsumk  10927  caucvgrelemcau  11724  fimaxre2  11971  climrecvg1n  12092  zsumdc  12129  fsum3  12132  isumss2  12138  fsum3ser  12142  sumpr  12158  sumtp  12159  fsum2dlemstep  12179  fsumiun  12222  isumlessdc  12241  zproddc  12324  fprodsplitdc  12341  fprodcl2lem  12350  fprod2dlemstep  12367  bezoutlemstep  12752  ennnfonelemim  13293  ctiunctal  13310  grppropd  13799  prdsmndd  14171  srgdilem  14247  srgrz  14262  srglz  14263  psrbagcon  14985  cnmpt11  15307  psmet0  15351  psmettri2  15352  mulcncflem  15631  mulcncf  15632  dedekindeulemuub  15641  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemlu  15654  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  plycoeid3  15781  fsumdvdsmul  16019  bj-charfundc  16748  bj-charfunbi  16751  nninffeq  16968  refeq  16978  iswomni0  17006  nconstwlpolem  17020