Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-iin | Unicode version | ||
| Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3971. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4002. Theorem intiin 4020 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.) |
| Ref | Expression |
|---|---|
| df-iin |
         
  |
, , ,() ()| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx |
. . 3
 | |
| 2 | cA |
. . 3
 | |
| 3 | cB |
. . 3
| |
| 4 | 1, 2, 3 | ciin 3970 |
. 2
|
| 5 | vy |
. . . . . 6
| |
| 6 | 5 | cv 1641 |
. . . . 5
|
| 7 | 6, 3 | wcel 1710 |
. . . 4
 |
| 8 | 7, 1, 2 | wral 2614 |
. . 3
|
| 9 | 8, 5 | cab 2339 |
. 2
|
| 10 | 4, 9 | wceq 1642 |
1
|
| Colors of variables: wff setvar class |
| This definition is referenced by: eliin 3974 iineq1 3983 iineq2 3986 nfiin 3996 nfii1 3998 dfiin2g 4000 cbviin 4004 intiin 4020 0iin 4024 viin 4025 iinxsng 4042 |
| Copyright terms: Public domain | W3C validator |