Definition df-i5 47

Description: Define relevance conditional.

Assertion

Ref	Expression
df-i5	(a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))

Detailed syntax breakdown of Definition df-i5

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi5 17	. 2 term  (a →5 b)
4	1, 2	wa 7	. . . 4 term  (a ∩ b)
5	1	wn 4	. . . . 5 term  a⊥
6	5, 2	wa 7	. . . 4 term  (a⊥ ∩ b)
7	4, 6	wo 6	. . 3 term  ((a ∩ b) ∪ (a⊥ ∩ b))
8	2	wn 4	. . . 4 term  b⊥
9	5, 8	wa 7	. . 3 term  (a⊥ ∩ b⊥ )
10	7, 9	wo 6	. 2 term  (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
11	3, 10	wb 1	1 wff  (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))

This definition is referenced by:  ud5lem0a 256  ud5lem0b 257  i5con 264  ud5lem0c 273  nom15 304  i5lei1 339  i5lei2 340  i5lei3 341  i5lei4 342  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem2 572  ud5lem3a 573  ud5lem3 576  u5lemaa 586  u5lemana 591  u5lemab 596  u5lemanb 601  u5lemoa 606  u5lemona 611  u5lemob 616  u5lemonb 621  u5lemc1 666  u5lemc1b 667  u5lemc2 672  u5lemc4 687  u5lemle2 701  u5lembi 707  u5lem5 747  u5lem6 751  u24lem 752

metamath.org