![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-res | Unicode version |
Description: Define the restriction of
a class. Definition 6.6(1) of [TakeutiZaring]
p. 24. For example ( F = { ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-res |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cres 4403 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | cvv 2612 |
. . . 4
![]() ![]() | |
5 | 2, 4 | cxp 4399 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | cin 2983 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4665 reseq2 4666 nfres 4673 csbresg 4674 res0 4675 opelres 4676 resres 4683 resundi 4684 resundir 4685 resindi 4686 resindir 4687 inres 4688 resiun1 4689 resiun2 4690 resss 4694 ssres 4696 ssres2 4697 relres 4698 xpssres 4704 resopab 4713 ssrnres 4827 imainrect 4830 xpima1 4831 xpima2m 4832 cnvcnv2 4838 resdmres 4876 nfvres 5282 ressnop0 5420 |
Copyright terms: Public domain | W3C validator |