Theorem r19.26 2677

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  r19.27v  2678  r19.28v  2679  r19.26-2  2680  r19.26-3  2681  ralbiim  2685  r19.27av  2686  reu8  3022  ssrab  3326  r19.28m  3617  r19.27m  3623  2ralunsn  3924  iuneq2  4028  cnvpom  5333  funco  5420  fncnv  5450  funimaexglem  5467  fnres  5503  fnopabg  5510  mpteqb  5799  eqfnfv3  5811  caoftrn  6339  iinerm  6885  ixpeq2  6998  ixpin  7009  rexanuz  11776  recvguniq  11783  cau3lem  11903  rexanre  12009  bezoutlemmo  12808  sqrt2irr  12966  pc11  13139  issubg3  14054  issubg4m  14055  ringsrg  14459  tgval2  15277  metequiv  15721  metequiv2  15722  mulcncflem  15833  2sqlem6  16444  vtxd0nedgbfi  16745  uspgr2wlkeq  16811  upgr2wlkdc  16823  bj-indind  17163