Theorem r19.26 2623

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 2560	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2560	. . 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 2562	. . 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 2475

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 1461  ax-gen 1463

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

This theorem is referenced by:  r19.27v  2624  r19.28v  2625  r19.26-2  2626  r19.26-3  2627  ralbiim  2631  r19.27av  2632  reu8  2960  ssrab  3261  r19.28m  3540  r19.27m  3546  2ralunsn  3828  iuneq2  3932  cnvpom  5212  funco  5298  fncnv  5324  funimaexglem  5341  fnres  5374  fnopabg  5381  mpteqb  5652  eqfnfv3  5661  caoftrn  6163  iinerm  6666  ixpeq2  6771  ixpin  6782  rexanuz  11153  recvguniq  11160  cau3lem  11279  rexanre  11385  bezoutlemmo  12173  sqrt2irr  12330  pc11  12500  issubg3  13322  issubg4m  13323  ringsrg  13603  tgval2  14287  metequiv  14731  metequiv2  14732  mulcncflem  14843  2sqlem6  15361  bj-indind  15578