Theorem r19.21bi 2594

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 2489	. . . 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 1581	. 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 2176   A.wral 2484

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

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

This theorem is referenced by:  rspec2  2595  rspec3  2596  r19.21be  2597  frind  4400  wepo  4407  wetrep  4408  ordelord  4429  ralxfr2d  4512  rexxfr2d  4513  funfveu  5591  fvmptelcdm  5735  f1oresrab  5747  isoselem  5891  mpoexw  6301  disjxp1  6324  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  xpf1o  6943  fimax2gtrilemstep  6999  supisoti  7114  difinfsn  7204  exmidomni  7246  cc3  7382  prcdnql  7599  prcunqu  7600  prdisj  7607  caucvgsrlembound  7909  caucvgsrlemoffgt1  7914  exbtwnzlemex  10394  monoord2  10633  iseqf1olemqk  10654  seq3f1olemqsumk  10659  caucvgrelemcau  11324  fimaxre2  11571  climrecvg1n  11692  zsumdc  11728  fsum3  11731  isumss2  11737  fsum3ser  11741  sumpr  11757  sumtp  11758  fsum2dlemstep  11778  fsumiun  11821  isumlessdc  11840  zproddc  11923  fprodsplitdc  11940  fprodcl2lem  11949  fprod2dlemstep  11966  bezoutlemstep  12351  ennnfonelemim  12828  ctiunctal  12845  prdsmndd  13313  grppropd  13382  srgdilem  13764  srgrz  13779  srglz  13780  cnmpt11  14788  psmet0  14832  psmettri2  14833  mulcncflem  15112  mulcncf  15113  dedekindeulemuub  15122  dedekindeulemlu  15126  dedekindicclemuub  15131  dedekindicclemlu  15135  limccnpcntop  15180  limccnp2lem  15181  limccnp2cntop  15182  plycoeid3  15262  fsumdvdsmul  15496  bj-charfundc  15781  bj-charfunbi  15784  nninffeq  15994  refeq  16004  iswomni0  16027  nconstwlpolem  16041