Description: Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020) (Proof shortened by BJ, 13-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elsymdifxor | |- ( A e. ( B /_\ C ) <-> ( A e. B \/_ A e. C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elsymdif | |- ( A e. ( B /_\ C ) <-> -. ( A e. B <-> A e. C ) ) |
|
| 2 | df-xor | |- ( ( A e. B \/_ A e. C ) <-> -. ( A e. B <-> A e. C ) ) |
|
| 3 | 1 2 | bitr4i | |- ( A e. ( B /_\ C ) <-> ( A e. B \/_ A e. C ) ) |