Theorem r19.26 2592

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 2529	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2529	. . 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 2531	. . 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 2444

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 1435  ax-gen 1437

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

This theorem is referenced by:  r19.27v  2593  r19.28v  2594  r19.26-2  2595  r19.26-3  2596  ralbiim  2600  r19.27av  2601  reu8  2922  ssrab  3220  r19.28m  3498  r19.27m  3504  2ralunsn  3778  iuneq2  3882  cnvpom  5146  funco  5228  fncnv  5254  funimaexglem  5271  fnres  5304  fnopabg  5311  mpteqb  5576  eqfnfv3  5585  caoftrn  6075  iinerm  6573  ixpeq2  6678  ixpin  6689  rexanuz  10930  recvguniq  10937  cau3lem  11056  rexanre  11162  bezoutlemmo  11939  sqrt2irr  12094  pc11  12262  tgval2  12691  metequiv  13135  metequiv2  13136  mulcncflem  13230  2sqlem6  13596  bj-indind  13814