Definition df-xor 1509

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 1540) and the constant false ⊥ (df-fal 1550), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1582), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1583), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1584), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1585). Contrast with ∧ (df-an 396), ∨ (df-or 847), → (wi 4), and ⊼ (df-nan 1489). (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 1508	. 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  1510  xorcom  1511  xorass  1512  excxor  1513  xor2  1514  xorneg2  1518  xorbi12i  1521  xorbi12d  1522  anxordi  1523  xorexmid  1524  truxortru  1582  truxorfal  1583  falxorfal  1585  hadbi  1595  elsymdifxor  4279  sadadd2lem2  16496  f1omvdco3  19491  bj-bixor  36557  wl-df3xor2  37435  wl-3xorbi  37439  wl-2xor  37449  tsxo3  38099  tsxo4  38100  oneptri  43218  ifpxorxorb  43473  or3or  43985  axorbtnotaiffb  46818  axorbciffatcxorb  46820  aisbnaxb  46826  abnotbtaxb  46830  abnotataxb  46831  afv2orxorb  47143