![]() |
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 2472 | . 2 class {𝑥 ∈ 𝐴 ∣ 𝜑} |
5 | 2 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cab 2175 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
9 | 4, 8 | wceq 1364 | 1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: rabid 2666 rabid2 2667 rabbi 2668 rabswap 2669 nfrab1 2670 nfrabxy 2671 rabbiia 2737 rabbidva2 2739 rabeqf 2742 cbvrab 2750 rabab 2773 elrabi 2905 elrabf 2906 elrab3t 2907 ralrab2 2917 rexrab2 2919 cbvrabcsf 3137 dfin5 3151 dfdif2 3152 ss2rab 3246 rabss 3247 ssrab 3248 rabss2 3253 ssrab2 3255 rabssab 3258 notab 3420 unrab 3421 inrab 3422 inrab2 3423 difrab 3424 dfrab2 3425 dfrab3 3426 notrab 3427 rabun2 3429 dfnul3 3440 rabn0r 3464 rabn0m 3465 rab0 3466 rabeq0 3467 dfif6 3551 rabsn 3674 reusn 3678 rabsneu 3680 elunirab 3837 elintrab 3871 ssintrab 3882 iunrab 3949 iinrabm 3964 intexrabim 4171 repizf2 4180 exss 4245 rabxp 4681 exse2 5020 mptpreima 5140 fndmin 5644 fncnvima2 5658 riotauni 5859 riotacl2 5866 snriota 5882 xp2 6199 unielxp 6200 dfopab2 6215 unfiexmid 6947 nnzrab 9308 nn0zrab 9309 shftlem 10860 shftuz 10861 shftdm 10866 negfi 11271 eqglact 13181 dfrhm2 13521 cnblcld 14512 if0ab 15035 bdcrab 15082 |
Copyright terms: Public domain | W3C validator |