Theorem r19.26 2583

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 108	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2520	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2520	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 304	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 138	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2522	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 123	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 125	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   A.wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429

This theorem depends on definitions:  df-bi 116  df-ral 2440

This theorem is referenced by:  r19.27v  2584  r19.28v  2585  r19.26-2  2586  r19.26-3  2587  ralbiim  2591  r19.27av  2592  reu8  2908  ssrab  3206  r19.28m  3483  r19.27m  3489  2ralunsn  3761  iuneq2  3865  cnvpom  5125  funco  5207  fncnv  5233  funimaexglem  5250  fnres  5283  fnopabg  5290  mpteqb  5555  eqfnfv3  5564  caoftrn  6051  iinerm  6545  ixpeq2  6650  ixpin  6661  rexanuz  10870  recvguniq  10877  cau3lem  10996  rexanre  11102  bezoutlemmo  11870  sqrt2irr  12016  tgval2  12411  metequiv  12855  metequiv2  12856  mulcncflem  12950  bj-indind  13467