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 2435 | . 2 |
5 | 2 | cv 1334 | . . . . 5 |
6 | 5, 3 | wcel 2128 | . . . 4 |
7 | 6, 1 | wi 4 | . . 3 |
8 | 7, 2 | wal 1333 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2445 rexnalim 2446 dfrex2dc 2448 ralbida 2451 ralbidv2 2459 ralbid2 2461 ralbii2 2467 r2alf 2474 hbral 2486 hbra1 2487 nfra1 2488 nfraldw 2489 nfraldxy 2490 nfraldya 2492 r3al 2501 alral 2502 rsp 2504 rgen 2510 rgen2a 2511 ralim 2516 ralimi2 2517 ralimdaa 2523 ralimdv2 2527 ralrimi 2528 r19.21t 2532 ralrimd 2535 r19.21bi 2545 rexim 2551 r19.23t 2564 r19.26m 2588 r19.32r 2603 rabid2 2633 rabbi 2634 raleqf 2648 cbvralf 2674 cbvralvw 2684 cbvraldva2 2687 ralv 2729 ceqsralt 2739 rspct 2809 rspc 2810 rspcimdv 2817 rspc2gv 2828 ralab 2872 ralab2 2876 ralrab2 2877 reu2 2900 reu6 2901 reu3 2902 rmo4 2905 reu8 2908 rmo3f 2909 rmoim 2913 2reuswapdc 2916 2rmorex 2918 ra5 3025 rmo2ilem 3026 rmo3 3028 cbvralcsf 3093 dfss3 3118 dfss3f 3120 ssabral 3199 ss2rab 3204 rabss 3205 ssrab 3206 dfdif3 3217 ralunb 3288 reuss2 3387 rabeq0 3423 rabxmdc 3425 disj 3442 disj1 3444 r19.2m 3480 r19.2mOLD 3481 r19.3rm 3482 ralidm 3494 rgenm 3496 ralf0 3497 ralm 3498 ralsnsg 3597 ralsns 3598 unissb 3803 dfint2 3810 elint2 3815 elintrab 3820 ssintrab 3831 dfiin2g 3883 invdisj 3960 dftr5 4066 trint 4078 repizf2lem 4123 ordsucim 4460 ordunisuc2r 4474 setindel 4498 elirr 4501 en2lp 4514 zfregfr 4534 tfi 4542 zfinf2 4549 peano2 4555 peano5 4558 find 4559 raliunxp 4728 dmopab3 4800 issref 4969 asymref 4972 dffun7 5198 funcnv 5232 funcnvuni 5240 fnres 5287 fnopabg 5294 rexrnmpt 5611 dffo3 5615 acexmidlem2 5822 nfixpxy 6663 pw1dc0el 6857 isomnimap 7081 ismkvmap 7098 iswomnimap 7110 fz1sbc 9999 isprm2 11998 istopg 12439 cbvrald 13404 decidr 13412 bdcint 13494 bdcriota 13500 bj-axempty 13510 bj-indind 13549 bj-ssom 13553 findset 13562 bj-nnord 13575 bj-inf2vn 13591 bj-inf2vn2 13592 bj-findis 13596 alsconv 13690 |
Copyright terms: Public domain | W3C validator |