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  11768  recvguniq  11775  cau3lem  11895  rexanre  12001  bezoutlemmo  12799  sqrt2irr  12957  pc11  13130  issubg3  14044  issubg4m  14045  ringsrg  14401  tgval2  15201  metequiv  15645  metequiv2  15646  mulcncflem  15757  2sqlem6  16337  vtxd0nedgbfi  16638  uspgr2wlkeq  16704  upgr2wlkdc  16716  bj-indind  17056