Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-rab | Unicode 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 | |
2 | vx | . . 3 | |
3 | cA | . . 3 | |
4 | 1, 2, 3 | crab 2446 | . 2 |
5 | 2 | cv 1341 | . . . . 5 |
6 | 5, 3 | wcel 2135 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | cab 2150 | . 2 |
9 | 4, 8 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: rabid 2639 rabid2 2640 rabbi 2641 rabswap 2642 nfrab1 2643 nfrabxy 2644 rabbiia 2706 rabbidva2 2708 rabeqf 2711 cbvrab 2719 rabab 2742 elrabi 2874 elrabf 2875 elrab3t 2876 ralrab2 2886 rexrab2 2888 cbvrabcsf 3105 dfin5 3118 dfdif2 3119 ss2rab 3213 rabss 3214 ssrab 3215 rabss2 3220 ssrab2 3222 rabssab 3225 notab 3387 unrab 3388 inrab 3389 inrab2 3390 difrab 3391 dfrab2 3392 dfrab3 3393 notrab 3394 rabun2 3396 dfnul3 3407 rabn0r 3430 rabn0m 3431 rab0 3432 rabeq0 3433 dfif6 3517 rabsn 3637 reusn 3641 rabsneu 3643 elunirab 3796 elintrab 3830 ssintrab 3841 iunrab 3907 iinrabm 3922 intexrabim 4126 repizf2 4135 exss 4199 rabxp 4635 exse2 4972 mptpreima 5091 fndmin 5586 fncnvima2 5600 riotauni 5798 riotacl2 5805 snriota 5821 xp2 6133 unielxp 6134 dfopab2 6149 unfiexmid 6874 nnzrab 9206 nn0zrab 9207 shftlem 10744 shftuz 10745 shftdm 10750 negfi 11155 cnblcld 13082 if0ab 13528 bdcrab 13575 |
Copyright terms: Public domain | W3C validator |