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  4353  wepo  4360  wetrep  4361  ordelord  4382  ralxfr2d  4465  rexxfr2d  4466  funfveu  5529  fvmptelcdm  5670  f1oresrab  5682  isoselem  5821  mpoexw  6214  disjxp1  6237  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  xpf1o  6844  fimax2gtrilemstep  6900  supisoti  7009  difinfsn  7099  exmidomni  7140  cc3  7267  prcdnql  7483  prcunqu  7484  prdisj  7491  caucvgsrlembound  7793  caucvgsrlemoffgt1  7798  exbtwnzlemex  10250  monoord2  10477  iseqf1olemqk  10494  seq3f1olemqsumk  10499  caucvgrelemcau  10989  fimaxre2  11235  climrecvg1n  11356  zsumdc  11392  fsum3  11395  isumss2  11401  fsum3ser  11405  sumpr  11421  sumtp  11422  fsum2dlemstep  11442  fsumiun  11485  isumlessdc  11504  zproddc  11587  fprodsplitdc  11604  fprodcl2lem  11613  fprod2dlemstep  11630  bezoutlemstep  11998  ennnfonelemim  12425  ctiunctal  12442  grppropd  12893  srgdilem  13152  srgrz  13167  srglz  13168  cnmpt11  13786  psmet0  13830  psmettri2  13831  mulcncflem  14093  mulcncf  14094  dedekindeulemuub  14098  dedekindeulemlu  14102  dedekindicclemuub  14107  dedekindicclemlu  14111  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  bj-charfundc  14563  bj-charfunbi  14566  nninffeq  14772  refeq  14779  iswomni0  14802  nconstwlpolem  14815