Theorem r19.26 2532

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 2469	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2469	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 302	. 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 2471	. . 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 2390

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

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

This theorem is referenced by:  r19.27v  2533  r19.28v  2534  r19.26-2  2535  r19.26-3  2536  ralbiim  2540  r19.27av  2541  reu8  2849  ssrab  3141  r19.28m  3418  r19.27m  3424  2ralunsn  3691  iuneq2  3795  cnvpom  5039  funco  5121  fncnv  5147  funimaexglem  5164  fnres  5197  fnopabg  5204  mpteqb  5465  eqfnfv3  5474  caoftrn  5961  iinerm  6455  ixpeq2  6560  ixpin  6571  rexanuz  10652  recvguniq  10659  cau3lem  10778  rexanre  10884  bezoutlemmo  11540  sqrt2irr  11686  tgval2  12063  metequiv  12484  metequiv2  12485  mulcncflem  12576  bj-indind  12822