Theorem r19.26 2747

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 443	. . . 4 |- ((ph /\ ps) -> ph)
2	1	ralimi 2690	. . 3 |- (A.x e. A (ph /\ ps) -> A.x e. A ph)
3		simpr 447	. . . 4 |- ((ph /\ ps) -> ps)
4	3	ralimi 2690	. . 3 |- (A.x e. A (ph /\ ps) -> A.x e. A ps)
5	2, 4	jca 518	. 2 |- (A.x e. A (ph /\ ps) -> (A.x e. A ph /\ A.x e. A ps))
6		pm3.2 434	. . . 4 |- (ph -> (ps -> (ph /\ ps)))
7	6	ral2imi 2691	. . 3 |- (A.x e. A ph -> (A.x e. A ps -> A.x e. A (ph /\ ps)))
8	7	imp 418	. 2 |- ((A.x e. A ph /\ A.x e. A ps) -> A.x e. A (ph /\ ps))
9	5, 8	impbii 180	1 |- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))

Syntax hints:   <-> wb 176   /\ wa 358  A.wral 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2620

This theorem is referenced by:  r19.26-2  2748  r19.26-3  2749  ralbiim  2752  r19.27av  2753  r19.35  2759  reu8  3033  ssrab  3345  r19.28z  3643  r19.28zv  3646  r19.27z  3649  r19.27zv  3650  2ralunsn  3881  iuneq2  3986  fncnv  5159  fnres  5200  fnopabg  5206  eqfnfv3  5395