Theorem r19.26 2596

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 2533	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2533	. . 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 2535	. . 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 2448

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 1440  ax-gen 1442

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

This theorem is referenced by:  r19.27v  2597  r19.28v  2598  r19.26-2  2599  r19.26-3  2600  ralbiim  2604  r19.27av  2605  reu8  2926  ssrab  3225  r19.28m  3504  r19.27m  3510  2ralunsn  3785  iuneq2  3889  cnvpom  5153  funco  5238  fncnv  5264  funimaexglem  5281  fnres  5314  fnopabg  5321  mpteqb  5586  eqfnfv3  5595  caoftrn  6086  iinerm  6585  ixpeq2  6690  ixpin  6701  rexanuz  10952  recvguniq  10959  cau3lem  11078  rexanre  11184  bezoutlemmo  11961  sqrt2irr  12116  pc11  12284  tgval2  12845  metequiv  13289  metequiv2  13290  mulcncflem  13384  2sqlem6  13750  bj-indind  13967