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  16378  f1omvdco3  19382  bj-bixor  36854  wl-df3xor2  37781  wl-3xorbi  37785  wl-2xor  37795  tsxo3  38451  tsxo4  38452  oneptri  43688  ifpxorxorb  43941  or3or  44453  axorbtnotaiffb  47337  axorbciffatcxorb  47339  aisbnaxb  47345  abnotbtaxb  47349  abnotataxb  47350  afv2orxorb  47662