Theorem r19.21bi 2621

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

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1396   e. wcel 2202   A.wral 2511

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

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

This theorem is referenced by:  rspec2  2622  rspec3  2623  r19.21be  2624  frind  4455  wepo  4462  wetrep  4463  ordelord  4484  ralxfr2d  4567  rexxfr2d  4568  funfveu  5661  fvmptelcdm  5808  f1oresrab  5820  isoselem  5971  mpoexw  6387  disjxp1  6410  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  xpf1o  7073  fimax2gtrilemstep  7133  supisoti  7269  difinfsn  7359  exmidomni  7401  cc3  7547  prcdnql  7764  prcunqu  7765  prdisj  7772  caucvgsrlembound  8074  caucvgsrlemoffgt1  8079  exbtwnzlemex  10572  monoord2  10811  iseqf1olemqk  10832  seq3f1olemqsumk  10837  caucvgrelemcau  11620  fimaxre2  11867  climrecvg1n  11988  zsumdc  12025  fsum3  12028  isumss2  12034  fsum3ser  12038  sumpr  12054  sumtp  12055  fsum2dlemstep  12075  fsumiun  12118  isumlessdc  12137  zproddc  12220  fprodsplitdc  12237  fprodcl2lem  12246  fprod2dlemstep  12263  bezoutlemstep  12648  ennnfonelemim  13125  ctiunctal  13142  prdsmndd  13611  grppropd  13680  srgdilem  14063  srgrz  14078  srglz  14079  psrbagcon  14772  cnmpt11  15094  psmet0  15138  psmettri2  15139  mulcncflem  15418  mulcncf  15419  dedekindeulemuub  15428  dedekindeulemlu  15432  dedekindicclemuub  15437  dedekindicclemlu  15441  limccnpcntop  15486  limccnp2lem  15487  limccnp2cntop  15488  plycoeid3  15568  fsumdvdsmul  15805  bj-charfundc  16524  bj-charfunbi  16527  nninffeq  16746  refeq  16756  iswomni0  16784  nconstwlpolem  16798