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 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-rab | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | crab 2420 | . 2 class {𝑥 ∈ 𝐴 ∣ 𝜑} |
5 | 2 | cv 1330 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1480 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cab 2125 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
9 | 4, 8 | wceq 1331 | 1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: rabid 2606 rabid2 2607 rabbi 2608 rabswap 2609 nfrab1 2610 nfrabxy 2611 rabbiia 2671 rabbidva2 2673 rabeqf 2676 cbvrab 2684 rabab 2707 elrabi 2837 elrabf 2838 elrab3t 2839 ralrab2 2849 rexrab2 2851 cbvrabcsf 3065 dfin5 3078 dfdif2 3079 ss2rab 3173 rabss 3174 ssrab 3175 rabss2 3180 ssrab2 3182 rabssab 3184 notab 3346 unrab 3347 inrab 3348 inrab2 3349 difrab 3350 dfrab2 3351 dfrab3 3352 notrab 3353 rabun2 3355 dfnul3 3366 rabn0r 3389 rabn0m 3390 rab0 3391 rabeq0 3392 dfif6 3476 rabsn 3590 reusn 3594 rabsneu 3596 elunirab 3749 elintrab 3783 ssintrab 3794 iunrab 3860 iinrabm 3875 intexrabim 4078 repizf2 4086 exss 4149 rabxp 4576 exse2 4913 mptpreima 5032 fndmin 5527 fncnvima2 5541 riotauni 5736 riotacl2 5743 snriota 5759 xp2 6071 unielxp 6072 dfopab2 6087 unfiexmid 6806 nnzrab 9078 nn0zrab 9079 shftlem 10588 shftuz 10589 shftdm 10594 negfi 10999 cnblcld 12704 bdcrab 13050 |
Copyright terms: Public domain | W3C validator |