Theorem r19.26 2634

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

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 1471  ax-gen 1473

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

This theorem is referenced by:  r19.27v  2635  r19.28v  2636  r19.26-2  2637  r19.26-3  2638  ralbiim  2642  r19.27av  2643  reu8  2976  ssrab  3279  r19.28m  3558  r19.27m  3564  2ralunsn  3853  iuneq2  3957  cnvpom  5244  funco  5330  fncnv  5359  funimaexglem  5376  fnres  5412  fnopabg  5419  mpteqb  5693  eqfnfv3  5702  caoftrn  6214  iinerm  6717  ixpeq2  6822  ixpin  6833  rexanuz  11414  recvguniq  11421  cau3lem  11540  rexanre  11646  bezoutlemmo  12442  sqrt2irr  12599  pc11  12769  issubg3  13643  issubg4m  13644  ringsrg  13924  tgval2  14638  metequiv  15082  metequiv2  15083  mulcncflem  15194  2sqlem6  15712  bj-indind  16067