Theorem r19.21bi 2520

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 2421	. . . 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 1537	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 123	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   A.wal 1329   e. wcel 1480   A.wral 2416

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

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

This theorem is referenced by:  rspec2  2521  rspec3  2522  r19.21be  2523  frind  4274  wepo  4281  wetrep  4282  ordelord  4303  ralxfr2d  4385  rexxfr2d  4386  funfveu  5434  fvmptelrn  5573  f1oresrab  5585  isoselem  5721  disjxp1  6133  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  xpf1o  6738  fimax2gtrilemstep  6794  supisoti  6897  difinfsn  6985  exmidomni  7014  prcdnql  7292  prcunqu  7293  prdisj  7300  caucvgsrlembound  7602  caucvgsrlemoffgt1  7607  exbtwnzlemex  10027  monoord2  10250  iseqf1olemqk  10267  seq3f1olemqsumk  10272  caucvgrelemcau  10752  fimaxre2  10998  climrecvg1n  11117  zsumdc  11153  fsum3  11156  isumss2  11162  fsum3ser  11166  sumpr  11182  sumtp  11183  fsum2dlemstep  11203  fsumiun  11246  isumlessdc  11265  bezoutlemstep  11685  ennnfonelemim  11937  cnmpt11  12452  psmet0  12496  psmettri2  12497  mulcncflem  12759  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  nninffeq  13216  refeq  13223