Theorem r19.26 2657

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

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 1493  ax-gen 1495

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

This theorem is referenced by:  r19.27v  2658  r19.28v  2659  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.27av  2666  reu8  2999  ssrab  3302  r19.28m  3581  r19.27m  3587  2ralunsn  3877  iuneq2  3981  cnvpom  5274  funco  5361  fncnv  5390  funimaexglem  5407  fnres  5443  fnopabg  5450  mpteqb  5730  eqfnfv3  5739  caoftrn  6260  iinerm  6767  ixpeq2  6872  ixpin  6883  rexanuz  11520  recvguniq  11527  cau3lem  11646  rexanre  11752  bezoutlemmo  12548  sqrt2irr  12705  pc11  12875  issubg3  13750  issubg4m  13751  ringsrg  14031  tgval2  14746  metequiv  15190  metequiv2  15191  mulcncflem  15302  2sqlem6  15820  vtxd0nedgbfi  16085  uspgr2wlkeq  16137  upgr2wlkdc  16147  bj-indind  16404