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  4209  sadadd2lem2  16363  f1omvdco3  19363  bj-bixor  36656  wl-df3xor2  37534  wl-3xorbi  37538  wl-2xor  37548  tsxo3  38199  tsxo4  38200  oneptri  43374  ifpxorxorb  43628  or3or  44140  axorbtnotaiffb  47027  axorbciffatcxorb  47029  aisbnaxb  47035  abnotbtaxb  47039  abnotataxb  47040  afv2orxorb  47352