Definition df-xor 1505

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 1536) and the constant false ⊥ (df-fal 1546), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1578), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1579), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1580), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1581). Contrast with ∧ (df-an 396), ∨ (df-or 845), → (wi 4), and ⊼ (df-nan 1485). (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 1504	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 205	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1506  xorcom  1507  xorass  1508  excxor  1509  xor2  1510  xorneg2  1514  xorbi12i  1517  xorbi12d  1518  anxordi  1519  xorexmid  1520  truxortru  1578  truxorfal  1579  falxorfal  1581  hadbi  1591  elsymdifxor  4242  sadadd2lem2  16390  f1omvdco3  19361  bj-bixor  35960  wl-df3xor2  36841  wl-3xorbi  36845  wl-2xor  36855  tsxo3  37501  tsxo4  37502  oneptri  42520  ifpxorxorb  42776  or3or  43288  axorbtnotaiffb  46123  axorbciffatcxorb  46125  aisbnaxb  46131  abnotbtaxb  46135  abnotataxb  46136  afv2orxorb  46446