![]() |
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 4479 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | cvv 2641 |
. . . 4
![]() ![]() | |
5 | 2, 4 | cxp 4475 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | cin 3020 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: reseq1 4749 reseq2 4750 nfres 4757 csbresg 4758 res0 4759 opelres 4760 resres 4767 resundi 4768 resundir 4769 resindi 4770 resindir 4771 inres 4772 resdifcom 4773 resiun1 4774 resiun2 4775 resss 4779 ssres 4781 ssres2 4782 relres 4783 xpssres 4790 resopab 4799 ssrnres 4917 imainrect 4920 xpima1 4921 xpima2m 4922 cnvcnv2 4928 resdmres 4966 nfvres 5386 ressnop0 5533 |
Copyright terms: Public domain | W3C validator |