Theorem r19.26 2558

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 108	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2495	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2495	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 304	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 138	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2497	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 123	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 125	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425

This theorem depends on definitions:  df-bi 116  df-ral 2421

This theorem is referenced by:  r19.27v  2559  r19.28v  2560  r19.26-2  2561  r19.26-3  2562  ralbiim  2566  r19.27av  2567  reu8  2880  ssrab  3175  r19.28m  3452  r19.27m  3458  2ralunsn  3725  iuneq2  3829  cnvpom  5081  funco  5163  fncnv  5189  funimaexglem  5206  fnres  5239  fnopabg  5246  mpteqb  5511  eqfnfv3  5520  caoftrn  6007  iinerm  6501  ixpeq2  6606  ixpin  6617  rexanuz  10760  recvguniq  10767  cau3lem  10886  rexanre  10992  bezoutlemmo  11694  sqrt2irr  11840  tgval2  12220  metequiv  12664  metequiv2  12665  mulcncflem  12759  bj-indind  13130