![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ral | GIF 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 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | wral 2468 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1362 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 105 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
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 5679 dffo3 5683 acexmidlem2 5892 nfixpxy 6742 pw1dc0el 6938 isomnimap 7164 ismkvmap 7181 iswomnimap 7193 fz1sbc 10125 nnwosdc 12071 isprm2 12148 istopg 13951 cbvrald 14993 decidr 15001 bdcint 15082 bdcriota 15088 bj-axempty 15098 bj-indind 15137 bj-ssom 15141 findset 15150 bj-nnord 15163 bj-inf2vn 15179 bj-inf2vn2 15180 bj-findis 15184 alsconv 15282 |
Copyright terms: Public domain | W3C validator |