Definition df-xor 1513

Description: Define exclusive disjunction (logical "xor"). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1544) and the constant false ⊥ (df-fal 1554), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1586), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1587), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1588), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1589). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1493). (Contributed by FL, 22-Nov-2010.)

Assertion

Ref	Expression
df-xor	⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wxo 1512	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1514  xorcom  1515  xorass  1516  excxor  1517  xor2  1518  xorneg2  1522  xorbi12i  1525  xorbi12d  1526  anxordi  1527  xorexmid  1528  truxortru  1586  truxorfal  1587  falxorfal  1589  hadbi  1599  elsymdifxor  4212  sadadd2lem2  16377  f1omvdco3  19378  bj-bixor  36791  wl-df3xor2  37670  wl-3xorbi  37674  wl-2xor  37684  tsxo3  38336  tsxo4  38337  oneptri  43495  ifpxorxorb  43748  or3or  44260  axorbtnotaiffb  47145  axorbciffatcxorb  47147  aisbnaxb  47153  abnotbtaxb  47157  abnotataxb  47158  afv2orxorb  47470