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  5330  funco  5417  fncnv  5447  funimaexglem  5464  fnres  5500  fnopabg  5507  mpteqb  5796  eqfnfv3  5808  caoftrn  6335  iinerm  6881  ixpeq2  6994  ixpin  7005  rexanuz  11754  recvguniq  11761  cau3lem  11880  rexanre  11986  bezoutlemmo  12783  sqrt2irr  12940  pc11  13110  issubg3  13995  issubg4m  13996  ringsrg  14352  tgval2  15152  metequiv  15596  metequiv2  15597  mulcncflem  15708  2sqlem6  16239  vtxd0nedgbfi  16540  uspgr2wlkeq  16606  upgr2wlkdc  16618  bj-indind  16958