![]() |
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 2468 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1363 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 2160 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wi 4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wal 1362 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2478 rexnalim 2479 dfrex2dc 2481 ralbida 2484 ralbidv2 2492 ralbid2 2494 ralbii2 2500 r2alf 2507 hbral 2519 hbra1 2520 nfra1 2521 nfraldw 2522 nfraldxy 2523 nfraldya 2525 r3al 2534 alral 2535 rsp 2537 rgen 2543 rgen2a 2544 ralim 2549 ralimi2 2550 ralimdaa 2556 ralimdv2 2560 ralrimi 2561 r19.21t 2565 ralrimd 2568 r19.21bi 2578 rexim 2584 r19.23t 2597 r19.26m 2621 r19.32r 2636 rabid2 2667 rabbi 2668 raleqf 2682 cbvralfw 2708 cbvralf 2710 cbvralvw 2722 cbvraldva2 2725 ralv 2769 ceqsralt 2779 rspct 2849 rspc 2850 rspcimdv 2857 rspc2gv 2868 ralab 2912 ralab2 2916 ralrab2 2917 reu2 2940 reu6 2941 reu3 2942 rmo4 2945 reu8 2948 rmo3f 2949 rmoim 2953 2reuswapdc 2956 2rmorex 2958 ra5 3066 rmo2ilem 3067 rmo3 3069 cbvralcsf 3134 dfss3 3160 dfss3f 3162 ssabral 3241 ss2rab 3246 rabss 3247 ssrab 3248 dfdif3 3260 ralunb 3331 reuss2 3430 rabeq0 3467 rabxmdc 3469 disj 3486 disj1 3488 r19.2m 3524 r19.2mOLD 3525 r19.3rm 3526 ralidm 3538 rgenm 3540 ralf0 3541 ralm 3542 ralsnsg 3644 ralsns 3645 unissb 3854 dfint2 3861 elint2 3866 elintrab 3871 ssintrab 3882 dfiin2g 3934 invdisj 4012 dftr5 4119 trint 4131 repizf2lem 4179 ordsucim 4517 ordunisuc2r 4531 setindel 4555 elirr 4558 en2lp 4571 zfregfr 4591 tfi 4599 zfinf2 4606 peano2 4612 peano5 4615 find 4616 raliunxp 4786 dmopab3 4858 issref 5029 asymref 5032 dffun7 5262 funcnv 5296 funcnvuni 5304 fnres 5351 fnopabg 5358 rexrnmpt 5680 dffo3 5684 acexmidlem2 5893 nfixpxy 6743 pw1dc0el 6939 isomnimap 7165 ismkvmap 7182 iswomnimap 7194 fz1sbc 10126 nnwosdc 12072 isprm2 12149 istopg 13956 cbvrald 14998 decidr 15006 bdcint 15087 bdcriota 15093 bj-axempty 15103 bj-indind 15142 bj-ssom 15146 findset 15155 bj-nnord 15168 bj-inf2vn 15184 bj-inf2vn2 15185 bj-findis 15189 alsconv 15287 |
Copyright terms: Public domain | W3C validator |