Theorem r19.26 2657

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 2593	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2593	. . 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 2595	. . 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 2508

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 1493  ax-gen 1495

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

This theorem is referenced by:  r19.27v  2658  r19.28v  2659  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.27av  2666  reu8  2999  ssrab  3302  r19.28m  3581  r19.27m  3587  2ralunsn  3877  iuneq2  3981  cnvpom  5271  funco  5358  fncnv  5387  funimaexglem  5404  fnres  5440  fnopabg  5447  mpteqb  5727  eqfnfv3  5736  caoftrn  6257  iinerm  6762  ixpeq2  6867  ixpin  6878  rexanuz  11515  recvguniq  11522  cau3lem  11641  rexanre  11747  bezoutlemmo  12543  sqrt2irr  12700  pc11  12870  issubg3  13745  issubg4m  13746  ringsrg  14026  tgval2  14741  metequiv  15185  metequiv2  15186  mulcncflem  15297  2sqlem6  15815  vtxd0nedgbfi  16059  uspgr2wlkeq  16111  upgr2wlkdc  16121  bj-indind  16378