![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ssdif | Structured version Unicode version |
Description: Difference law for subsets. (Contributed by NM, 28-May-1998.) |
Ref | Expression |
---|---|
ssdif |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3457 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim1d 564 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eldif 3445 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | eldif 3445 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4g 270 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | ssrdv 3469 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-v 3078 df-dif 3438 df-in 3442 df-ss 3449 |
This theorem is referenced by: ssdifd 3599 php 7604 pssnn 7641 mapfienOLD 8037 fin1a2lem13 8691 axcclem 8736 isercolllem3 13261 mvdco 16069 dprdres 16646 dpjidcl 16678 dpjidclOLD 16685 ablfac1eulem 16694 lspsnat 17348 lbsextlem2 17362 lbsextlem3 17363 mplmonmul 17666 cnsubdrglem 17988 clscon 19165 2ndcdisj2 19192 kqdisj 19436 nulmbl2 21150 i1f1 21300 itg11 21301 itg1climres 21324 limcresi 21492 dvreslem 21516 dvres2lem 21517 dvaddbr 21544 dvmulbr 21545 lhop 21620 elqaa 21920 imadifxp 26089 xrge00 26291 eulerpartlemmf 26901 eulerpartlemgf 26905 mblfinlem3 28577 mblfinlem4 28578 ismblfin 28579 cnambfre 28587 divrngidl 28975 cntzsdrg 29706 bj-2upln1upl 32834 |
Copyright terms: Public domain | W3C validator |