![]() |
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 2349 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1284 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1434 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1283 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 103 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2359 rexnalim 2360 ralbida 2363 ralbidv2 2371 ralbii2 2377 r2alf 2384 hbral 2396 hbra1 2397 nfra1 2398 nfraldxy 2399 nfraldya 2401 r3al 2409 alral 2410 rsp 2412 rgen 2417 rgen2a 2418 ralim 2423 ralimi2 2424 ralimdaa 2429 ralimdv2 2432 ralrimi 2433 r19.21t 2437 ralrimd 2440 r19.21bi 2450 rexim 2456 r19.23t 2468 r19.26m 2489 r19.32r 2502 rabid2 2531 rabbi 2532 raleqf 2546 cbvralf 2572 cbvraldva2 2582 ralv 2617 ceqsralt 2627 rspct 2695 rspc 2696 rspcimdv 2703 rspc2gv 2713 ralab 2753 ralab2 2757 ralrab2 2758 reu2 2781 reu6 2782 reu3 2783 rmo4 2786 reu8 2789 rmoim 2792 2reuswapdc 2795 2rmorex 2797 ra5 2903 rmo2ilem 2904 rmo3 2906 cbvralcsf 2965 dfss3 2990 dfss3f 2992 ssabral 3066 ss2rab 3071 rabss 3072 ssrab 3073 ralunb 3154 reuss2 3251 rabeq0 3281 rabxmdc 3283 disj 3299 disj1 3301 r19.2m 3336 r19.3rm 3337 ralidm 3349 rgenm 3351 ralf0 3352 ralm 3353 ralsnsg 3438 ralsns 3439 unissb 3639 dfint2 3646 elint2 3651 elintrab 3656 ssintrab 3667 dfiin2g 3719 invdisj 3788 dftr5 3886 trint 3898 repizf2lem 3943 ordsucim 4252 ordunisuc2r 4266 setindel 4289 elirr 4292 en2lp 4305 zfregfr 4324 tfi 4331 zfinf2 4338 peano2 4344 peano5 4347 find 4348 raliunxp 4505 dmopab3 4576 issref 4737 asymref 4740 dffun7 4958 funcnv 4991 funcnvuni 4999 fnres 5046 fnopabg 5053 rexrnmpt 5342 dffo3 5346 acexmidlem2 5540 fz1sbc 9189 isprm2 10643 cbvrald 10749 decidr 10757 bdcint 10826 bdcriota 10832 bj-axempty 10842 bj-indind 10885 bj-ssom 10889 findset 10898 bj-nnord 10911 bj-inf2vn 10927 bj-inf2vn2 10928 bj-findis 10932 alsconv 10949 |
Copyright terms: Public domain | W3C validator |