Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-in | Unicode version | ||
| Description: Define the intersection of two classes. See elin 3219 for membership. (Contributed by SF, 10-Jan-2015.) |
| Ref | Expression |
|---|---|
| df-in |
       ∼ &ncap |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | cB |
. . 3
| |
| 3 | 1, 2 | cin 3208 |
. 2
|
| 4 | 1, 2 | cnin 3204 |
. . 3
&ncap |
| 5 | 4 | ccompl 3205 |
. 2
∼ &ncap |
| 6 | 3, 5 | wceq 1642 |
1
 ∼
&ncap |
| Colors of variables: wff setvar class |
| This definition is referenced by: elin 3219 nfin 3230 difeq1 3246 difeq2 3247 dfin5 3545 incompl 4073 inexg 4100 |
| Copyright terms: Public domain | W3C validator |