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  5725  eqfnfv3  5734  caoftrn  6251  iinerm  6754  ixpeq2  6859  ixpin  6870  rexanuz  11499  recvguniq  11506  cau3lem  11625  rexanre  11731  bezoutlemmo  12527  sqrt2irr  12684  pc11  12854  issubg3  13729  issubg4m  13730  ringsrg  14010  tgval2  14725  metequiv  15169  metequiv2  15170  mulcncflem  15281  2sqlem6  15799  uspgr2wlkeq  16076  bj-indind  16295