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  6886  ixpeq2  7000  ixpin  7011  rexanuz  11775  recvguniq  11782  cau3lem  11902  rexanre  12008  bezoutlemmo  12807  sqrt2irr  12965  pc11  13138  issubg3  14053  issubg4m  14054  ringsrg  14458  tgval2  15294  metequiv  15738  metequiv2  15739  mulcncflem  15850  2sqlem6  16461  vtxd0nedgbfi  16762  uspgr2wlkeq  16828  upgr2wlkdc  16840  bj-indind  17180