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 2397 | . 2 class {𝑥 ∈ 𝐴 ∣ 𝜑} |
5 | 2 | cv 1315 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1465 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cab 2103 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
9 | 4, 8 | wceq 1316 | 1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: rabid 2583 rabid2 2584 rabbi 2585 rabswap 2586 nfrab1 2587 nfrabxy 2588 rabbiia 2645 rabbidva2 2647 rabeqf 2650 cbvrab 2658 rabab 2681 elrabi 2810 elrabf 2811 elrab3t 2812 ralrab2 2822 rexrab2 2824 cbvrabcsf 3035 dfin5 3048 dfdif2 3049 ss2rab 3143 rabss 3144 ssrab 3145 rabss2 3150 ssrab2 3152 rabssab 3154 notab 3316 unrab 3317 inrab 3318 inrab2 3319 difrab 3320 dfrab2 3321 dfrab3 3322 notrab 3323 rabun2 3325 dfnul3 3336 rabn0r 3359 rabn0m 3360 rab0 3361 rabeq0 3362 dfif6 3446 rabsn 3560 reusn 3564 rabsneu 3566 elunirab 3719 elintrab 3753 ssintrab 3764 iunrab 3830 iinrabm 3845 intexrabim 4048 repizf2 4056 exss 4119 rabxp 4546 exse2 4883 mptpreima 5002 fndmin 5495 fncnvima2 5509 riotauni 5704 riotacl2 5711 snriota 5727 xp2 6039 unielxp 6040 dfopab2 6055 unfiexmid 6774 nnzrab 9036 nn0zrab 9037 shftlem 10543 shftuz 10544 shftdm 10549 negfi 10954 cnblcld 12615 bdcrab 12946 |
Copyright terms: Public domain | W3C validator |