![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-rab | GIF version |
Description: Define a restricted class abstraction (class builder), which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-rab | ⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | vx | . . 3 setvar x | |
3 | cA | . . 3 class A | |
4 | 1, 2, 3 | crab 2304 | . 2 class {x ∈ A ∣ φ} |
5 | 2 | cv 1241 | . . . . 5 class x |
6 | 5, 3 | wcel 1390 | . . . 4 wff x ∈ A |
7 | 6, 1 | wa 97 | . . 3 wff (x ∈ A ∧ φ) |
8 | 7, 2 | cab 2023 | . 2 class {x ∣ (x ∈ A ∧ φ)} |
9 | 4, 8 | wceq 1242 | 1 wff {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)} |
Colors of variables: wff set class |
This definition is referenced by: rabid 2479 rabid2 2480 rabbi 2481 rabswap 2482 nfrab1 2483 nfrabxy 2484 rabbiia 2541 rabeqf 2544 cbvrab 2549 rabab 2569 elrabi 2689 elrabf 2690 elrab3t 2691 ralrab2 2700 rexrab2 2702 cbvrabcsf 2905 dfin5 2919 dfdif2 2920 ss2rab 3010 rabss 3011 ssrab 3012 rabss2 3017 ssrab2 3019 rabssab 3021 notab 3201 unrab 3202 inrab 3203 inrab2 3204 difrab 3205 dfrab2 3206 dfrab3 3207 notrab 3208 rabun2 3210 dfnul3 3221 rabn0r 3238 rabn0m 3239 rab0 3240 rabeq0 3241 dfif6 3327 rabsn 3428 reusn 3432 rabsneu 3434 elunirab 3584 elintrab 3618 ssintrab 3629 iunrab 3695 iinrabm 3710 intexrabim 3898 repizf2 3906 exss 3954 rabxp 4323 exse2 4642 mptpreima 4757 fndmin 5217 fncnvima2 5231 riotauni 5417 riotacl2 5424 snriota 5440 xp2 5741 unielxp 5742 dfopab2 5757 nnzrab 8045 nn0zrab 8046 bdcrab 9307 |
Copyright terms: Public domain | W3C validator |