![]() |
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 2417 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1331 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1481 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1330 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2427 rexnalim 2428 dfrex2dc 2429 ralbida 2432 ralbidv2 2440 ralbid2 2442 ralbii2 2448 r2alf 2455 hbral 2467 hbra1 2468 nfra1 2469 nfraldxy 2470 nfraldya 2472 r3al 2480 alral 2481 rsp 2483 rgen 2488 rgen2a 2489 ralim 2494 ralimi2 2495 ralimdaa 2501 ralimdv2 2505 ralrimi 2506 r19.21t 2510 ralrimd 2513 r19.21bi 2523 rexim 2529 r19.23t 2542 r19.26m 2566 r19.32r 2581 rabid2 2610 rabbi 2611 raleqf 2625 cbvralf 2651 cbvraldva2 2664 ralv 2706 ceqsralt 2716 rspct 2786 rspc 2787 rspcimdv 2794 rspc2gv 2805 ralab 2848 ralab2 2852 ralrab2 2853 reu2 2876 reu6 2877 reu3 2878 rmo4 2881 reu8 2884 rmo3f 2885 rmoim 2889 2reuswapdc 2892 2rmorex 2894 ra5 3001 rmo2ilem 3002 rmo3 3004 cbvralcsf 3067 dfss3 3092 dfss3f 3094 ssabral 3173 ss2rab 3178 rabss 3179 ssrab 3180 dfdif3 3191 ralunb 3262 reuss2 3361 rabeq0 3397 rabxmdc 3399 disj 3416 disj1 3418 r19.2m 3454 r19.2mOLD 3455 r19.3rm 3456 ralidm 3468 rgenm 3470 ralf0 3471 ralm 3472 ralsnsg 3568 ralsns 3569 unissb 3774 dfint2 3781 elint2 3786 elintrab 3791 ssintrab 3802 dfiin2g 3854 invdisj 3931 dftr5 4037 trint 4049 repizf2lem 4093 ordsucim 4424 ordunisuc2r 4438 setindel 4461 elirr 4464 en2lp 4477 zfregfr 4496 tfi 4504 zfinf2 4511 peano2 4517 peano5 4520 find 4521 raliunxp 4688 dmopab3 4760 issref 4929 asymref 4932 dffun7 5158 funcnv 5192 funcnvuni 5200 fnres 5247 fnopabg 5254 rexrnmpt 5571 dffo3 5575 acexmidlem2 5779 nfixpxy 6619 isomnimap 7017 ismkvmap 7036 iswomnimap 7048 fz1sbc 9907 isprm2 11834 istopg 12205 cbvrald 13166 decidr 13174 bdcint 13246 bdcriota 13252 bj-axempty 13262 bj-indind 13301 bj-ssom 13305 findset 13314 bj-nnord 13327 bj-inf2vn 13343 bj-inf2vn2 13344 bj-findis 13348 alsconv 13437 |
Copyright terms: Public domain | W3C validator |