![]() |
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 | ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | vx | . . 3 setvar x | |
3 | cA | . . 3 class A | |
4 | 1, 2, 3 | wral 2300 | . 2 wff ∀x ∈ A φ |
5 | 2 | cv 1241 | . . . . 5 class x |
6 | 5, 3 | wcel 1390 | . . . 4 wff x ∈ A |
7 | 6, 1 | wi 4 | . . 3 wff (x ∈ A → φ) |
8 | 7, 2 | wal 1240 | . 2 wff ∀x(x ∈ A → φ) |
9 | 4, 8 | wb 98 | 1 wff (∀x ∈ A φ ↔ ∀x(x ∈ A → φ)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2310 rexnalim 2311 ralbida 2314 ralbidv2 2322 ralbii2 2328 r2alf 2335 hbral 2347 hbra1 2348 nfra1 2349 nfraldxy 2350 nfraldya 2352 r3al 2360 alral 2361 rsp 2363 rgen 2368 rgen2a 2369 ralim 2374 ralimi2 2375 ralimdaa 2380 ralimdv2 2383 ralrimi 2384 r19.21t 2388 ralrimd 2391 r19.21bi 2401 rexim 2407 r19.23t 2417 r19.26m 2438 r19.32r 2451 rabid2 2480 rabbi 2481 raleqf 2495 cbvralf 2521 cbvraldva2 2531 ralv 2565 ceqsralt 2575 rspct 2643 rspc 2644 rspcimdv 2651 ralab 2695 ralab2 2699 ralrab2 2700 reu2 2723 reu6 2724 reu3 2725 rmo4 2728 reu8 2731 rmoim 2734 2reuswapdc 2737 2rmorex 2739 ra5 2840 rmo2ilem 2841 rmo3 2843 cbvralcsf 2902 dfss3 2929 dfss3f 2931 ssabral 3005 ss2rab 3010 rabss 3011 ssrab 3012 ralunb 3118 reuss2 3211 rabeq0 3241 rabxmdc 3243 disj 3262 disj1 3264 r19.2m 3303 r19.3rm 3304 ralidm 3315 rgenm 3317 ralf0 3318 ralm 3319 ralsns 3399 unissb 3601 dfint2 3608 elint2 3613 elintrab 3618 ssintrab 3629 dfiin2g 3681 invdisj 3750 dftr5 3848 trint 3860 repizf2lem 3905 ordsucim 4192 ordunisuc2r 4205 setindel 4221 elirr 4224 en2lp 4232 tfi 4248 zfinf2 4255 peano2 4261 peano5 4264 find 4265 raliunxp 4420 dmopab3 4491 issref 4650 asymref 4653 dffun7 4871 funcnv 4903 funcnvuni 4911 fnres 4958 fnopabg 4965 rexrnmpt 5253 dffo3 5257 acexmidlem2 5452 fz1sbc 8728 cbvrald 9262 bdcint 9332 bdcriota 9338 bj-axempty 9348 bj-indind 9391 bj-ssom 9395 peano5setOLD 9400 findset 9405 bj-nnord 9418 bj-inf2vn 9434 bj-inf2vn2 9435 bj-findis 9439 alsconv 9453 |
Copyright terms: Public domain | W3C validator |