Definition df-i0 42

Description: Define classical conditional.

Assertion

Ref	Expression
df-i0	(a →0 b) = (a⊥ ∪ b)

Detailed syntax breakdown of Definition df-i0

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi0 12	. 2 term  (a →0 b)
4	1	wn 4	. . 3 term  a⊥
5	4, 2	wo 6	. 2 term  (a⊥ ∪ b)
6	3, 5	wb 1	1 wff  (a →0 b) = (a⊥ ∪ b)

This definition is referenced by:  nom10 299  nom40 317  i0cmtrcom 477  u12lem 753  3vded21 799  3vded22 800  3vded3 801  3vroa 813  negant0 839  distoa 924  d3oa 975  oadist2a 987  oacom 991  oacom3 993  oagen1 994  oagen2 996  oadistd 1003

metamath.org