Theorem r19.21bi 2554

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 2449	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 121	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1546	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 123	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   A.wal 1341   e. wcel 2136   A.wral 2444

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

This theorem depends on definitions:  df-bi 116  df-ral 2449

This theorem is referenced by:  rspec2  2555  rspec3  2556  r19.21be  2557  frind  4330  wepo  4337  wetrep  4338  ordelord  4359  ralxfr2d  4442  rexxfr2d  4443  funfveu  5499  fvmptelrn  5638  f1oresrab  5650  isoselem  5788  mpoexw  6181  disjxp1  6204  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  xpf1o  6810  fimax2gtrilemstep  6866  supisoti  6975  difinfsn  7065  exmidomni  7106  cc3  7209  prcdnql  7425  prcunqu  7426  prdisj  7433  caucvgsrlembound  7735  caucvgsrlemoffgt1  7740  exbtwnzlemex  10185  monoord2  10412  iseqf1olemqk  10429  seq3f1olemqsumk  10434  caucvgrelemcau  10922  fimaxre2  11168  climrecvg1n  11289  zsumdc  11325  fsum3  11328  isumss2  11334  fsum3ser  11338  sumpr  11354  sumtp  11355  fsum2dlemstep  11375  fsumiun  11418  isumlessdc  11437  zproddc  11520  fprodsplitdc  11537  fprodcl2lem  11546  fprod2dlemstep  11563  bezoutlemstep  11930  ennnfonelemim  12357  ctiunctal  12374  cnmpt11  12923  psmet0  12967  psmettri2  12968  mulcncflem  13230  mulcncf  13231  dedekindeulemuub  13235  dedekindeulemlu  13239  dedekindicclemuub  13244  dedekindicclemlu  13248  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  bj-charfundc  13690  bj-charfunbi  13693  nninffeq  13900  refeq  13907  iswomni0  13930  nconstwlpolem  13943