Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ral | Unicode version |
Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
df-ral |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | cA | . . 3 | |
4 | 1, 2, 3 | wral 2448 | . 2 |
5 | 2 | cv 1347 | . . . . 5 |
6 | 5, 3 | wcel 2141 | . . . 4 |
7 | 6, 1 | wi 4 | . . 3 |
8 | 7, 2 | wal 1346 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2458 rexnalim 2459 dfrex2dc 2461 ralbida 2464 ralbidv2 2472 ralbid2 2474 ralbii2 2480 r2alf 2487 hbral 2499 hbra1 2500 nfra1 2501 nfraldw 2502 nfraldxy 2503 nfraldya 2505 r3al 2514 alral 2515 rsp 2517 rgen 2523 rgen2a 2524 ralim 2529 ralimi2 2530 ralimdaa 2536 ralimdv2 2540 ralrimi 2541 r19.21t 2545 ralrimd 2548 r19.21bi 2558 rexim 2564 r19.23t 2577 r19.26m 2601 r19.32r 2616 rabid2 2646 rabbi 2647 raleqf 2661 cbvralfw 2687 cbvralf 2689 cbvralvw 2700 cbvraldva2 2703 ralv 2747 ceqsralt 2757 rspct 2827 rspc 2828 rspcimdv 2835 rspc2gv 2846 ralab 2890 ralab2 2894 ralrab2 2895 reu2 2918 reu6 2919 reu3 2920 rmo4 2923 reu8 2926 rmo3f 2927 rmoim 2931 2reuswapdc 2934 2rmorex 2936 ra5 3043 rmo2ilem 3044 rmo3 3046 cbvralcsf 3111 dfss3 3137 dfss3f 3139 ssabral 3218 ss2rab 3223 rabss 3224 ssrab 3225 dfdif3 3237 ralunb 3308 reuss2 3407 rabeq0 3444 rabxmdc 3446 disj 3463 disj1 3465 r19.2m 3501 r19.2mOLD 3502 r19.3rm 3503 ralidm 3515 rgenm 3517 ralf0 3518 ralm 3519 ralsnsg 3620 ralsns 3621 unissb 3826 dfint2 3833 elint2 3838 elintrab 3843 ssintrab 3854 dfiin2g 3906 invdisj 3983 dftr5 4090 trint 4102 repizf2lem 4147 ordsucim 4484 ordunisuc2r 4498 setindel 4522 elirr 4525 en2lp 4538 zfregfr 4558 tfi 4566 zfinf2 4573 peano2 4579 peano5 4582 find 4583 raliunxp 4752 dmopab3 4824 issref 4993 asymref 4996 dffun7 5225 funcnv 5259 funcnvuni 5267 fnres 5314 fnopabg 5321 rexrnmpt 5639 dffo3 5643 acexmidlem2 5850 nfixpxy 6695 pw1dc0el 6889 isomnimap 7113 ismkvmap 7130 iswomnimap 7142 fz1sbc 10052 nnwosdc 11994 isprm2 12071 istopg 12791 cbvrald 13823 decidr 13831 bdcint 13912 bdcriota 13918 bj-axempty 13928 bj-indind 13967 bj-ssom 13971 findset 13980 bj-nnord 13993 bj-inf2vn 14009 bj-inf2vn2 14010 bj-findis 14014 alsconv 14109 |
Copyright terms: Public domain | W3C validator |