Metamath Proof Explorer


Theorem distel

Description: Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el and elirrv .) (Contributed by Scott Fenton, 15-Dec-2010)

Ref Expression
Assertion distel
|- ( -. A. y y = x <-> -. A. y -. x e. y )

Proof

Step Hyp Ref Expression
1 el
 |-  E. z x e. z
2 df-ex
 |-  ( E. z x e. z <-> -. A. z -. x e. z )
3 nfnae
 |-  F/ y -. A. y y = x
4 dveel1
 |-  ( -. A. y y = x -> ( x e. z -> A. y x e. z ) )
5 3 4 nf5d
 |-  ( -. A. y y = x -> F/ y x e. z )
6 5 nfnd
 |-  ( -. A. y y = x -> F/ y -. x e. z )
7 elequ2
 |-  ( z = y -> ( x e. z <-> x e. y ) )
8 7 notbid
 |-  ( z = y -> ( -. x e. z <-> -. x e. y ) )
9 8 a1i
 |-  ( -. A. y y = x -> ( z = y -> ( -. x e. z <-> -. x e. y ) ) )
10 3 6 9 cbvald
 |-  ( -. A. y y = x -> ( A. z -. x e. z <-> A. y -. x e. y ) )
11 10 notbid
 |-  ( -. A. y y = x -> ( -. A. z -. x e. z <-> -. A. y -. x e. y ) )
12 2 11 syl5bb
 |-  ( -. A. y y = x -> ( E. z x e. z <-> -. A. y -. x e. y ) )
13 1 12 mpbii
 |-  ( -. A. y y = x -> -. A. y -. x e. y )
14 elirrv
 |-  -. y e. y
15 elequ1
 |-  ( y = x -> ( y e. y <-> x e. y ) )
16 14 15 mtbii
 |-  ( y = x -> -. x e. y )
17 16 alimi
 |-  ( A. y y = x -> A. y -. x e. y )
18 17 con3i
 |-  ( -. A. y -. x e. y -> -. A. y y = x )
19 13 18 impbii
 |-  ( -. A. y y = x <-> -. A. y -. x e. y )