Theorem zfregs2

Description: Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by Wolf Lammen, 27-Sep-2013)

	Ref	Expression
Assertion	zfregs2	|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )

Proof

Step	Hyp	Ref	Expression
1		zfregs	|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )
2		incom	|- ( x i^i A ) = ( A i^i x )
3	2	eqeq1i	|- ( ( x i^i A ) = (/) <-> ( A i^i x ) = (/) )
4	3	rexbii	|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A ( A i^i x ) = (/) )
5	1 4	sylib	|- ( A =/= (/) -> E. x e. A ( A i^i x ) = (/) )
6		disj1	|- ( ( A i^i x ) = (/) <-> A. y ( y e. A -> -. y e. x ) )
7	6	rexbii	|- ( E. x e. A ( A i^i x ) = (/) <-> E. x e. A A. y ( y e. A -> -. y e. x ) )
8	5 7	sylib	|- ( A =/= (/) -> E. x e. A A. y ( y e. A -> -. y e. x ) )
9		alinexa	|- ( A. y ( y e. A -> -. y e. x ) <-> -. E. y ( y e. A /\ y e. x ) )
10	9	rexbii	|- ( E. x e. A A. y ( y e. A -> -. y e. x ) <-> E. x e. A -. E. y ( y e. A /\ y e. x ) )
11	8 10	sylib	|- ( A =/= (/) -> E. x e. A -. E. y ( y e. A /\ y e. x ) )
12		dfrex2	|- ( E. x e. A -. E. y ( y e. A /\ y e. x ) <-> -. A. x e. A -. -. E. y ( y e. A /\ y e. x ) )
13	11 12	sylib	|- ( A =/= (/) -> -. A. x e. A -. -. E. y ( y e. A /\ y e. x ) )
14		notnotb	|- ( E. y ( y e. A /\ y e. x ) <-> -. -. E. y ( y e. A /\ y e. x ) )
15	14	ralbii	|- ( A. x e. A E. y ( y e. A /\ y e. x ) <-> A. x e. A -. -. E. y ( y e. A /\ y e. x ) )
16	13 15	sylnibr	|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )