Description: Alternate proof of difid . (Contributed by David Abernethy, 17-Jun-2012) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | difidALT | |- ( A \ A ) = (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdif2 | |- ( A \ A ) = { x e. A | -. x e. A } |
|
2 | dfnul3 | |- (/) = { x e. A | -. x e. A } |
|
3 | 1 2 | eqtr4i | |- ( A \ A ) = (/) |