Theorem r19.26 2603

Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.26	|- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		simpl 109	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2540	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2540	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 306	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 139	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2542	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 124	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 126	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   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-ia3 108  ax-5 1447  ax-gen 1449

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

This theorem is referenced by:  r19.27v  2604  r19.28v  2605  r19.26-2  2606  r19.26-3  2607  ralbiim  2611  r19.27av  2612  reu8  2935  ssrab  3235  r19.28m  3514  r19.27m  3520  2ralunsn  3800  iuneq2  3904  cnvpom  5173  funco  5258  fncnv  5284  funimaexglem  5301  fnres  5334  fnopabg  5341  mpteqb  5608  eqfnfv3  5617  caoftrn  6110  iinerm  6609  ixpeq2  6714  ixpin  6725  rexanuz  10999  recvguniq  11006  cau3lem  11125  rexanre  11231  bezoutlemmo  12009  sqrt2irr  12164  pc11  12332  issubg3  13057  issubg4m  13058  ringsrg  13229  tgval2  13636  metequiv  14080  metequiv2  14081  mulcncflem  14175  2sqlem6  14552  bj-indind  14769