Theorem r19.21bi 2638

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   A.wal 1400   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1563

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rspec2  2639  rspec3  2640  r19.21be  2641  frind  4499  wepo  4506  wetrep  4507  ordelord  4528  ralxfr2d  4612  rexxfr2d  4613  funfveu  5711  fvmptelcdm  5864  f1oresrab  5876  isoselem  6029  mpoexw  6453  disjxp1  6476  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  xpf1o  7150  fimax2gtrilemstep  7211  supisoti  7356  difinfsn  7446  exmidomni  7488  cc3  7640  prcdnql  7857  prcunqu  7858  prdisj  7865  caucvgsrlembound  8167  caucvgsrlemoffgt1  8172  exbtwnzlemex  10700  monoord2  10943  iseqf1olemqk  10964  seq3f1olemqsumk  10969  caucvgrelemcau  11767  fimaxre2  12015  climrecvg1n  12138  zsumdc  12175  fsum3  12178  isumss2  12184  fsum3ser  12188  sumpr  12204  sumtp  12205  fsum2dlemstep  12225  fsumiun  12268  isumlessdc  12287  zproddc  12370  fprodsplitdc  12387  fprodcl2lem  12396  fprod2dlemstep  12413  bezoutlemstep  12798  ennnfonelemim  13372  ctiunctal  13389  grppropd  13880  gsummptfidmsplit  14253  prdsmndd  14300  srgdilem  14379  srgrz  14394  srglz  14395  psrbagcon  15174  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  cnmpt11  15526  psmet0  15570  psmettri2  15571  mulcncflem  15850  mulcncf  15851  dedekindeulemuub  15860  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemlu  15873  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  plycoeid3  16000  fsumdvdsmul  16302  bj-charfundc  17056  bj-charfunbi  17059  nninffeq  17286  refeq  17296  iswomni0  17325  nconstwlpolem  17339