Theorem r19.26 2435

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 102	. . . 4 |- ((ph /\ ps) -> ph)
2	1	ralimi 2378	. . 3 |- (A.x e. A (ph /\ ps) -> A.x e. A ph)
3		simpr 103	. . . 4 |- ((ph /\ ps) -> ps)
4	3	ralimi 2378	. . 3 |- (A.x e. A (ph /\ ps) -> A.x e. A ps)
5	2, 4	jca 290	. 2 |- (A.x e. A (ph /\ ps) -> (A.x e. A ph /\ A.x e. A ps))
6		pm3.2 126	. . . 4 |- (ph -> (ps -> (ph /\ ps)))
7	6	ral2imi 2379	. . 3 |- (A.x e. A ph -> (A.x e. A ps -> A.x e. A (ph /\ ps)))
8	7	imp 115	. 2 |- ((A.x e. A ph /\ A.x e. A ps) -> A.x e. A (ph /\ ps))
9	5, 8	impbii 117	1 |- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))

Syntax hints:   /\ wa 97   <-> wb 98  A.wral 2300

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335

This theorem depends on definitions:  df-bi 110  df-ral 2305

This theorem is referenced by:  r19.26-2  2436  r19.26-3  2437  ralbiim  2441  r19.27av  2442  reu8  2731  ssrab  3012  r19.28m  3305  r19.27m  3310  2ralunsn  3560  iuneq2  3664  cnvpom  4803  funco  4883  fncnv  4908  funimaexglem  4925  fnres  4958  fnopabg  4965  mpteqb  5204  eqfnfv3  5210  caoftrn  5678  iinerm  6114