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  cc3  7083  prcdnql  7299  prcunqu  7300  prdisj  7307  caucvgsrlembound  7609  caucvgsrlemoffgt1  7614  exbtwnzlemex  10034  monoord2  10257  iseqf1olemqk  10274  seq3f1olemqsumk  10279  caucvgrelemcau  10759  fimaxre2  11005  climrecvg1n  11124  zsumdc  11160  fsum3  11163  isumss2  11169  fsum3ser  11173  sumpr  11189  sumtp  11190  fsum2dlemstep  11210  fsumiun  11253  isumlessdc  11272  bezoutlemstep  11692  ennnfonelemim  11944  ctiunctal  11961  cnmpt11  12462  psmet0  12506  psmettri2  12507  mulcncflem  12769  mulcncf  12770  dedekindeulemuub  12774  dedekindeulemlu  12778  dedekindicclemuub  12783  dedekindicclemlu  12787  limccnpcntop  12823  limccnp2lem  12824  limccnp2cntop  12825  nninffeq  13226  refeq  13233