Theorem r19.26 2485

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 107	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2426	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 108	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2426	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 300	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 137	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2427	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 122	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 124	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 102   <-> wb 103   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115  df-ral 2353

This theorem is referenced by:  r19.26-2  2486  r19.26-3  2487  ralbiim  2491  r19.27av  2492  reu8  2788  ssrab  3072  r19.28m  3331  r19.27m  3336  2ralunsn  3590  iuneq2  3694  cnvpom  4880  funco  4960  fncnv  4985  funimaexglem  5002  fnres  5035  fnopabg  5042  mpteqb  5282  eqfnfv3  5288  caoftrn  5756  iinerm  6201  rexanuz  9874  recvguniq  9881  cau3lem  10000  rexanre  10106  bezoutlemmo  10395  sqrt2irr  10541  bj-indind  10727