Definition df-i0 43

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 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  lem4.6.6i0j1  1086  lem4.6.6i0j2  1087  lem4.6.6i0j3  1088  lem4.6.6i0j4  1089  lem4.6.6i1j0  1090  lem4.6.6i1j3  1092  lem4.6.6i2j0  1093  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j0  1096  lem4.6.6i3j1  1097  lem4.6.6i4j0  1098  lem4.6.6i4j2  1099