Definition df-or 197

Description: Define disjunction (logical 'or'). This is our first use of the biconditional connective in a definition; we use it in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute (¬ φ → ψ) for (φ ∨ ψ), we end up with an instance of previously proved theorem pm4.2 148. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Definition of [Margaris] p. 49.

Assertion

Ref	Expression
df-or	⊢ ((φ ∨ ψ) ↔ (¬ φ → ψ))

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3	1, 2	wo 195	. 2 wff (φ ∨ ψ)
4	1	wn 1	. . 3 wff ¬ φ
5	4, 2	wi 2	. 2 wff (¬ φ → ψ)
6	3, 5	wb 127	1 wff ((φ ∨ ψ) ↔ (¬ φ → ψ))

This definition is referenced by:  dfor2 199  ori 200  orri 201  ord 202  orrd 203  imor 204  oridm 208  orcom 209  orel1 212  orbi2i 214  or12 217  pm3.48 430  ordi 452  orbi2d 466  orcana 509  biorf 551  hbor 703  19.30 764  19.32 765  sbor 887  r19.32v 1297  undif4 1744  sotric 2148  so 2152  dfwe2 2187  wereu 2197  ordsseleq 2227  ordtri1 2231  ordtri3 2234  limsuclem 2360  tfinds 2401  sdomdomtr 3370  kmlem13 3592  ltapr 3945  infxpidmlem12 4944  elat2 5739

metamath.org