Definition df-xor 1512

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 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1585), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1586), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1587), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1588). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1492). (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 1511	. 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  1513  xorcom  1514  xorass  1515  excxor  1516  xor2  1517  xorneg2  1521  xorbi12i  1524  xorbi12d  1525  anxordi  1526  xorexmid  1527  truxortru  1585  truxorfal  1586  falxorfal  1588  hadbi  1598  elsymdifxor  4213  sadadd2lem2  16379  f1omvdco3  19346  bj-bixor  36564  wl-df3xor2  37442  wl-3xorbi  37446  wl-2xor  37456  tsxo3  38118  tsxo4  38119  oneptri  43230  ifpxorxorb  43484  or3or  43996  axorbtnotaiffb  46888  axorbciffatcxorb  46890  aisbnaxb  46896  abnotbtaxb  46900  abnotataxb  46901  afv2orxorb  47213