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  10249  monoord2  10476  iseqf1olemqk  10493  seq3f1olemqsumk  10498  caucvgrelemcau  10988  fimaxre2  11234  climrecvg1n  11355  zsumdc  11391  fsum3  11394  isumss2  11400  fsum3ser  11404  sumpr  11420  sumtp  11421  fsum2dlemstep  11441  fsumiun  11484  isumlessdc  11503  zproddc  11586  fprodsplitdc  11603  fprodcl2lem  11612  fprod2dlemstep  11629  bezoutlemstep  11997  ennnfonelemim  12424  ctiunctal  12441  grppropd  12892  srgdilem  13150  srgrz  13165  srglz  13166  cnmpt11  13753  psmet0  13797  psmettri2  13798  mulcncflem  14060  mulcncf  14061  dedekindeulemuub  14065  dedekindeulemlu  14069  dedekindicclemuub  14074  dedekindicclemlu  14078  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  bj-charfundc  14530  bj-charfunbi  14533  nninffeq  14739  refeq  14746  iswomni0  14769  nconstwlpolem  14782