Theorem r19.26 2659

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

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

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

This theorem is referenced by:  r19.27v  2660  r19.28v  2661  r19.26-2  2662  r19.26-3  2663  ralbiim  2667  r19.27av  2668  reu8  3002  ssrab  3305  r19.28m  3584  r19.27m  3590  2ralunsn  3882  iuneq2  3986  cnvpom  5279  funco  5366  fncnv  5396  funimaexglem  5413  fnres  5449  fnopabg  5456  mpteqb  5737  eqfnfv3  5746  caoftrn  6268  iinerm  6776  ixpeq2  6881  ixpin  6892  rexanuz  11566  recvguniq  11573  cau3lem  11692  rexanre  11798  bezoutlemmo  12595  sqrt2irr  12752  pc11  12922  issubg3  13797  issubg4m  13798  ringsrg  14079  tgval2  14794  metequiv  15238  metequiv2  15239  mulcncflem  15350  2sqlem6  15868  vtxd0nedgbfi  16169  uspgr2wlkeq  16235  upgr2wlkdc  16247  bj-indind  16578