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  4497  wepo  4504  wetrep  4505  ordelord  4526  ralxfr2d  4610  rexxfr2d  4611  funfveu  5708  fvmptelcdm  5861  f1oresrab  5873  isoselem  6026  mpoexw  6449  disjxp1  6472  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  xpf1o  7144  fimax2gtrilemstep  7205  supisoti  7351  difinfsn  7441  exmidomni  7483  cc3  7635  prcdnql  7852  prcunqu  7853  prdisj  7860  caucvgsrlembound  8162  caucvgsrlemoffgt1  8167  exbtwnzlemex  10695  monoord2  10938  iseqf1olemqk  10959  seq3f1olemqsumk  10964  caucvgrelemcau  11762  fimaxre2  12010  climrecvg1n  12133  zsumdc  12170  fsum3  12173  isumss2  12179  fsum3ser  12183  sumpr  12199  sumtp  12200  fsum2dlemstep  12220  fsumiun  12263  isumlessdc  12282  zproddc  12365  fprodsplitdc  12382  fprodcl2lem  12391  fprod2dlemstep  12408  bezoutlemstep  12793  ennnfonelemim  13367  ctiunctal  13384  grppropd  13875  prdsmndd  14278  srgdilem  14357  srgrz  14372  srglz  14373  psrbagcon  15146  cnmpt11  15475  psmet0  15519  psmettri2  15520  mulcncflem  15799  mulcncf  15800  dedekindeulemuub  15809  dedekindeulemlu  15813  dedekindicclemuub  15818  dedekindicclemlu  15822  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  plycoeid3  15949  fsumdvdsmul  16246  bj-charfundc  17000  bj-charfunbi  17003  nninffeq  17229  refeq  17239  iswomni0  17268  nconstwlpolem  17282