Theorem r19.26 2660

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

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 1496  ax-gen 1498

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

This theorem is referenced by:  r19.27v  2661  r19.28v  2662  r19.26-2  2663  r19.26-3  2664  ralbiim  2668  r19.27av  2669  reu8  3003  ssrab  3306  r19.28m  3586  r19.27m  3592  2ralunsn  3887  iuneq2  3991  cnvpom  5286  funco  5373  fncnv  5403  funimaexglem  5420  fnres  5456  fnopabg  5463  mpteqb  5746  eqfnfv3  5755  caoftrn  6277  iinerm  6819  ixpeq2  6924  ixpin  6935  rexanuz  11628  recvguniq  11635  cau3lem  11754  rexanre  11860  bezoutlemmo  12657  sqrt2irr  12814  pc11  12984  issubg3  13859  issubg4m  13860  ringsrg  14141  tgval2  14862  metequiv  15306  metequiv2  15307  mulcncflem  15418  2sqlem6  15939  vtxd0nedgbfi  16240  uspgr2wlkeq  16306  upgr2wlkdc  16318  bj-indind  16648