Theorem r19.21bi 2618

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 2513	. . . 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 1604	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 124	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1393   e. wcel 2200   A.wral 2508

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

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

This theorem is referenced by:  rspec2  2619  rspec3  2620  r19.21be  2621  frind  4443  wepo  4450  wetrep  4451  ordelord  4472  ralxfr2d  4555  rexxfr2d  4556  funfveu  5642  fvmptelcdm  5790  f1oresrab  5802  isoselem  5950  mpoexw  6365  disjxp1  6388  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  xpf1o  7013  fimax2gtrilemstep  7071  supisoti  7188  difinfsn  7278  exmidomni  7320  cc3  7465  prcdnql  7682  prcunqu  7683  prdisj  7690  caucvgsrlembound  7992  caucvgsrlemoffgt1  7997  exbtwnzlemex  10481  monoord2  10720  iseqf1olemqk  10741  seq3f1olemqsumk  10746  caucvgrelemcau  11507  fimaxre2  11754  climrecvg1n  11875  zsumdc  11911  fsum3  11914  isumss2  11920  fsum3ser  11924  sumpr  11940  sumtp  11941  fsum2dlemstep  11961  fsumiun  12004  isumlessdc  12023  zproddc  12106  fprodsplitdc  12123  fprodcl2lem  12132  fprod2dlemstep  12149  bezoutlemstep  12534  ennnfonelemim  13011  ctiunctal  13028  prdsmndd  13497  grppropd  13566  srgdilem  13948  srgrz  13963  srglz  13964  cnmpt11  14973  psmet0  15017  psmettri2  15018  mulcncflem  15297  mulcncf  15298  dedekindeulemuub  15307  dedekindeulemlu  15311  dedekindicclemuub  15316  dedekindicclemlu  15320  limccnpcntop  15365  limccnp2lem  15366  limccnp2cntop  15367  plycoeid3  15447  fsumdvdsmul  15681  bj-charfundc  16254  bj-charfunbi  16257  nninffeq  16474  refeq  16484  iswomni0  16507  nconstwlpolem  16521