Theorem r19.21bi 2596

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

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1371   e. wcel 2178   A.wral 2486

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

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

This theorem is referenced by:  rspec2  2597  rspec3  2598  r19.21be  2599  frind  4417  wepo  4424  wetrep  4425  ordelord  4446  ralxfr2d  4529  rexxfr2d  4530  funfveu  5612  fvmptelcdm  5756  f1oresrab  5768  isoselem  5912  mpoexw  6322  disjxp1  6345  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  xpf1o  6966  fimax2gtrilemstep  7023  supisoti  7138  difinfsn  7228  exmidomni  7270  cc3  7415  prcdnql  7632  prcunqu  7633  prdisj  7640  caucvgsrlembound  7942  caucvgsrlemoffgt1  7947  exbtwnzlemex  10429  monoord2  10668  iseqf1olemqk  10689  seq3f1olemqsumk  10694  caucvgrelemcau  11406  fimaxre2  11653  climrecvg1n  11774  zsumdc  11810  fsum3  11813  isumss2  11819  fsum3ser  11823  sumpr  11839  sumtp  11840  fsum2dlemstep  11860  fsumiun  11903  isumlessdc  11922  zproddc  12005  fprodsplitdc  12022  fprodcl2lem  12031  fprod2dlemstep  12048  bezoutlemstep  12433  ennnfonelemim  12910  ctiunctal  12927  prdsmndd  13395  grppropd  13464  srgdilem  13846  srgrz  13861  srglz  13862  cnmpt11  14870  psmet0  14914  psmettri2  14915  mulcncflem  15194  mulcncf  15195  dedekindeulemuub  15204  dedekindeulemlu  15208  dedekindicclemuub  15213  dedekindicclemlu  15217  limccnpcntop  15262  limccnp2lem  15263  limccnp2cntop  15264  plycoeid3  15344  fsumdvdsmul  15578  bj-charfundc  15943  bj-charfunbi  15946  nninffeq  16159  refeq  16169  iswomni0  16192  nconstwlpolem  16206