Theorem r19.21bi 2565

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

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1351   e. wcel 2148   A.wral 2455

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

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

This theorem is referenced by:  rspec2  2566  rspec3  2567  r19.21be  2568  frind  4352  wepo  4359  wetrep  4360  ordelord  4381  ralxfr2d  4464  rexxfr2d  4465  funfveu  5528  fvmptelcdm  5669  f1oresrab  5681  isoselem  5820  mpoexw  6213  disjxp1  6236  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  xpf1o  6843  fimax2gtrilemstep  6899  supisoti  7008  difinfsn  7098  exmidomni  7139  cc3  7266  prcdnql  7482  prcunqu  7483  prdisj  7490  caucvgsrlembound  7792  caucvgsrlemoffgt1  7797  exbtwnzlemex  10247  monoord2  10474  iseqf1olemqk  10491  seq3f1olemqsumk  10496  caucvgrelemcau  10984  fimaxre2  11230  climrecvg1n  11351  zsumdc  11387  fsum3  11390  isumss2  11396  fsum3ser  11400  sumpr  11416  sumtp  11417  fsum2dlemstep  11437  fsumiun  11480  isumlessdc  11499  zproddc  11582  fprodsplitdc  11599  fprodcl2lem  11608  fprod2dlemstep  11625  bezoutlemstep  11992  ennnfonelemim  12419  ctiunctal  12436  grppropd  12847  srgdilem  13105  srgrz  13120  srglz  13121  cnmpt11  13676  psmet0  13720  psmettri2  13721  mulcncflem  13983  mulcncf  13984  dedekindeulemuub  13988  dedekindeulemlu  13992  dedekindicclemuub  13997  dedekindicclemlu  14001  limccnpcntop  14037  limccnp2lem  14038  limccnp2cntop  14039  bj-charfundc  14442  bj-charfunbi  14445  nninffeq  14651  refeq  14658  iswomni0  14681  nconstwlpolem  14694