MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-or Unicode version

Definition df-or 361
Description: Define disjunction (logical 'or'). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true ?Error: 2 = 3 \/ 4 = 4 ) ^ This math symbol is not active (i.e. was not declared in this scope). that (2=3\/4=4) (ex-or 21765). After we define the constant ?Error: T. ^^ This math symbol is not active (i.e. was not declared in this scope). ?Error: F. ^^ This math symbol is not active (i.e. was not declared in this scope). true (df-tru 1329) and the constant false (df-fal 1330), we will be able to prove these truth table values: ?Error: T. \/ T. ) <-> T. ) ^^ This math symbol is not active (i.e. was not declared in this scope). ?Error: T. \/ F. ) <-> T. ) ^^ This math symbol is not active (i.e. was not declared in this scope). (( \/ )<-> ) (truortru 1350), (( \/ )<-> ) ?Error: F. \/ T. ) <-> T. ) ^^ This math symbol is not active (i.e. was not declared in this scope). (truorfal 1351), (( \/ )<-> ) (falortru 1352), and ?Error: F. \/ F. ) <-> F. ) ^^ This math symbol is not active (i.e. was not declared in this scope). (( \/ )<-> ) (falorfal 1353).

This is our first use of the biconditional connective in a definition; we use the biconditional connective 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 biid 229. This is the justification for the definition, along with the fact that it introduces a new symbol ?Error: -/\ ^^^ This math symbol is not active (i.e. was not declared in this scope). \/. Contrast with /\ (df-an 362), -> (wi 4), -/\ ?Error: \/_ ^^^ This math symbol is not active (i.e. was not declared in this scope). (df-nan 1298), and \/_ (df-xor 1315) . (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
df-or

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wo 359 . 2
41wn 3 . . 3
54, 2wi 4 . 2
63, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  pm4.64  363  pm2.53  364  pm2.54  365  ori  366  orri  367  ord  368  imor  403  mtord  643  orbi2d  684  orimdi  822  ordi  836  pm5.17  860  pm5.6  880  orbidi  900  cador  1401  cadan  1402  19.30  1616  19.43  1617  nfor  1862  19.32  1901  dfsb3  2120  sbor  2149  neor  2699  r19.30  2864  r19.32v  2865  r19.43  2874  dfif2  3771  disjor  4231  sotric  4574  sotrieq  4575  isso2i  4580  soxp  6513  unxpwdom2  7609  cflim2  8198  cfpwsdom  8514  ltapr  8977  ltxrlt  9201  isprm4  13144  euclemma  13163  islpi  17249  restntr  17282  alexsubALTlem2  18115  alexsubALTlem3  18116  2bornot2b  21794  disjorf  24066  funcnv5mpt  24136  ballotlemodife  25015  3orit  25429  dfon2lem5  25674  ecase13d  26583  elicc3  26587  nn0prpw  26593  orfa  26959  unitresl  26962  cnf1dd  26970  tsim1  26979  tsbi3  26984  pm10.541  27874  r19.32  28255  sborNEW7  29963  dfsb3NEW7  30036
  Copyright terms: Public domain W3C validator