Definition df-xor 1519

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 1550) and the constant false ⊥ (df-fal 1560), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1592), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1593), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1594), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1595). Contrast with ∧ (df-an 397), ∨ (df-or 854), → (wi 4), and ⊼ (df-nan 1499). (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 1518	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 207	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 207	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1520  xorcom  1521  xorass  1522  excxor  1523  xor2  1524  xorneg2  1528  xorbi12i  1531  xorbi12d  1532  anxordi  1533  xorexmid  1534  truxortru  1592  truxorfal  1593  falxorfal  1595  hadbi  1605  elsymdifxor  4195  sadadd2lem2  16417  f1omvdco3  19422  bj-bixor  36909  wl-df3xor2  37838  wl-3xorbi  37842  wl-2xor  37852  tsxo3  38513  tsxo4  38514  oneptri  43709  ifpxorxorb  43962  or3or  44474  axorbtnotaiffb  47373  axorbciffatcxorb  47375  aisbnaxb  47381  abnotbtaxb  47385  abnotataxb  47386  afv2orxorb  47698