Theorem r19.21bi 2594

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

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1371   e. wcel 2176   A.wral 2484

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

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

This theorem is referenced by:  rspec2  2595  rspec3  2596  r19.21be  2597  frind  4399  wepo  4406  wetrep  4407  ordelord  4428  ralxfr2d  4511  rexxfr2d  4512  funfveu  5589  fvmptelcdm  5733  f1oresrab  5745  isoselem  5889  mpoexw  6299  disjxp1  6322  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  xpf1o  6941  fimax2gtrilemstep  6997  supisoti  7112  difinfsn  7202  exmidomni  7244  cc3  7380  prcdnql  7597  prcunqu  7598  prdisj  7605  caucvgsrlembound  7907  caucvgsrlemoffgt1  7912  exbtwnzlemex  10392  monoord2  10631  iseqf1olemqk  10652  seq3f1olemqsumk  10657  caucvgrelemcau  11291  fimaxre2  11538  climrecvg1n  11659  zsumdc  11695  fsum3  11698  isumss2  11704  fsum3ser  11708  sumpr  11724  sumtp  11725  fsum2dlemstep  11745  fsumiun  11788  isumlessdc  11807  zproddc  11890  fprodsplitdc  11907  fprodcl2lem  11916  fprod2dlemstep  11933  bezoutlemstep  12318  ennnfonelemim  12795  ctiunctal  12812  prdsmndd  13280  grppropd  13349  srgdilem  13731  srgrz  13746  srglz  13747  cnmpt11  14755  psmet0  14799  psmettri2  14800  mulcncflem  15079  mulcncf  15080  dedekindeulemuub  15089  dedekindeulemlu  15093  dedekindicclemuub  15098  dedekindicclemlu  15102  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  plycoeid3  15229  fsumdvdsmul  15463  bj-charfundc  15744  bj-charfunbi  15747  nninffeq  15957  refeq  15967  iswomni0  15990  nconstwlpolem  16004