Definition df-i1 43

Description: Define Sasaki (Mittelstaedt) conditional.

Assertion

Ref	Expression
df-i1	(a →1 b) = (a⊥ ∪ (a ∩ b))

Detailed syntax breakdown of Definition df-i1

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi1 13	. 2 term  (a →1 b)
4	1	wn 4	. . 3 term  a⊥
5	1, 2	wa 7	. . 3 term  (a ∩ b)
6	4, 5	wo 6	. 2 term  (a⊥ ∪ (a ∩ b))
7	3, 6	wb 1	1 wff  (a →1 b) = (a⊥ ∪ (a ∩ b))

This definition is referenced by:  wlem1 235  ud1lem0a 247  ud1lem0b 248  i1i2 258  0i1 265  1i1 266  i1id 267  ud1lem0c 269  wql1lem 279  wql2lem4 283  oaidlem1 286  womle2a 287  nom10 299  nom11 300  nom12 301  nom13 302  nom14 303  nom15 304  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  nom25 310  go1 335  i1or 337  i5lei1 339  2vwomr1a 345  2vwomr2a 346  wr5-2v 348  woml6 418  ud1lem1 542  ud1lem2 543  ud1lem3 544  u1lemaa 582  u1lemana 587  u1lemab 592  u1lemanb 597  u1lemoa 602  u1lemona 607  u1lemob 612  u1lemonb 617  u1lemc1 662  u1lemc2 668  u1lemc4 683  u1lemc6 688  comi12 689  comi1 691  u1lemle2 697  u1lembi 702  u12lembi 708  u21lembi 709  u1lemn1b 712  u1lem2 726  u1lem3 731  u1lem4 739  u1lem5 743  u12lem 753  u1lem7 754  u1lem8 758  u1lem9a 759  u1lem9b 760  u1lem11 762  u3lem13a 771  u3lem13b 772  bi1o1a 780  i2i1i1 782  3vth9 794  3vded11 796  3vded12 797  1oa 802  mlalem 814  sa5 818  salem1 819  sadm3 820  bi3 821  bi4 822  imp3 823  orbi 824  i1orni1 829  negantlem1 830  negantlem2 831  negantlem3 832  negantlem4 833  negantlem9 841  negantlem10 843  neg3antlem2 847  neg3ant1 848  elimconslem 849  elimcons 850  elimcons2 851  comanblem1 852  comanb 854  mlaconjolem 867  cancellem 873  gomaex3h7 888  gomaex3h10 891  gomaex3lem3 896  gomaex3lem4 897  gomaex3 904  oas 905  oat 907  oatr 908  oaidlem2 911  oaidlem2g 912  oa3to4lem1 925  oa3to4lem2 926  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4btoc 946  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-2to2s 970  d3oa 975  axoa4a 1016

metamath.org