Theorem r19.21bi 2620

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

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1395   e. wcel 2202   A.wral 2510

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

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

This theorem is referenced by:  rspec2  2621  rspec3  2622  r19.21be  2623  frind  4449  wepo  4456  wetrep  4457  ordelord  4478  ralxfr2d  4561  rexxfr2d  4562  funfveu  5652  fvmptelcdm  5800  f1oresrab  5812  isoselem  5961  mpoexw  6378  disjxp1  6401  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  xpf1o  7030  fimax2gtrilemstep  7090  supisoti  7209  difinfsn  7299  exmidomni  7341  cc3  7487  prcdnql  7704  prcunqu  7705  prdisj  7712  caucvgsrlembound  8014  caucvgsrlemoffgt1  8019  exbtwnzlemex  10510  monoord2  10749  iseqf1olemqk  10770  seq3f1olemqsumk  10775  caucvgrelemcau  11558  fimaxre2  11805  climrecvg1n  11926  zsumdc  11963  fsum3  11966  isumss2  11972  fsum3ser  11976  sumpr  11992  sumtp  11993  fsum2dlemstep  12013  fsumiun  12056  isumlessdc  12075  zproddc  12158  fprodsplitdc  12175  fprodcl2lem  12184  fprod2dlemstep  12201  bezoutlemstep  12586  ennnfonelemim  13063  ctiunctal  13080  prdsmndd  13549  grppropd  13618  srgdilem  14001  srgrz  14016  srglz  14017  cnmpt11  15026  psmet0  15070  psmettri2  15071  mulcncflem  15350  mulcncf  15351  dedekindeulemuub  15360  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemlu  15373  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  plycoeid3  15500  fsumdvdsmul  15734  bj-charfundc  16454  bj-charfunbi  16457  nninffeq  16673  refeq  16683  iswomni0  16707  nconstwlpolem  16721