Definition df-xor 1514

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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1587), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1588), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1589), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1590). Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and ⊼ (df-nan 1494). (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 1513	. 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  1515  xorcom  1516  xorass  1517  excxor  1518  xor2  1519  xorneg2  1523  xorbi12i  1526  xorbi12d  1527  anxordi  1528  xorexmid  1529  truxortru  1587  truxorfal  1588  falxorfal  1590  hadbi  1600  elsymdifxor  4201  sadadd2lem2  16410  f1omvdco3  19415  bj-bixor  36872  wl-df3xor2  37799  wl-3xorbi  37803  wl-2xor  37813  tsxo3  38474  tsxo4  38475  oneptri  43703  ifpxorxorb  43956  or3or  44468  axorbtnotaiffb  47363  axorbciffatcxorb  47365  aisbnaxb  47371  abnotbtaxb  47375  abnotataxb  47376  afv2orxorb  47688