Definition df-xor 1501

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 399), ∨ (df-or 844), → (wi 4), and ⊼ (df-nan 1481). (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 1500	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 208	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1502  xorcom  1503  xorass  1504  excxor  1505  xor2  1506  xorneg2  1510  xorbi12i  1513  xorbi12d  1514  anxordi  1515  xorexmid  1516  truxortru  1578  truxorfal  1579  falxorfal  1581  hadbi  1594  elsymdifxor  4225  sadadd2lem2  15793  f1omvdco3  18571  bj-bixor  33920  tsxo3  35411  tsxo4  35412  ifpxorxorb  39870  or3or  40364  axorbtnotaiffb  43133  axorbciffatcxorb  43135  aisbnaxb  43141  abnotbtaxb  43145  abnotataxb  43146  afv2orxorb  43421