This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )