Theorem r19.26 2632

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 2569	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2569	. . 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 2571	. . 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 2484

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 1470  ax-gen 1472

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

This theorem is referenced by:  r19.27v  2633  r19.28v  2634  r19.26-2  2635  r19.26-3  2636  ralbiim  2640  r19.27av  2641  reu8  2969  ssrab  3271  r19.28m  3550  r19.27m  3556  2ralunsn  3839  iuneq2  3943  cnvpom  5226  funco  5312  fncnv  5341  funimaexglem  5358  fnres  5394  fnopabg  5401  mpteqb  5672  eqfnfv3  5681  caoftrn  6193  iinerm  6696  ixpeq2  6801  ixpin  6812  rexanuz  11332  recvguniq  11339  cau3lem  11458  rexanre  11564  bezoutlemmo  12360  sqrt2irr  12517  pc11  12687  issubg3  13561  issubg4m  13562  ringsrg  13842  tgval2  14556  metequiv  15000  metequiv2  15001  mulcncflem  15112  2sqlem6  15630  bj-indind  15905