Definition df-i0 43

Description: Define classical conditional. (Contributed by NM, 31-Oct-1998.)

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 11	. 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  307  nom40  325  i0cmtrcom  495  u12lem  771  3vded21  817  3vded22  818  3vded3  819  3vroa  831  negant0  857  distoa  944  d3oa  995  oadist2a  1007  oacom  1011  oacom3  1013  oagen1  1014  oagen2  1016  oadistd  1023  lem3.3.2  1046  lem3.3.3  1052  lem3.3.7i0e1  1057  lem3.4.1  1075  thm3.8i1lem  1080  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101