![]() |
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 2370 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1295 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1445 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1294 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2380 rexnalim 2381 dfrex2dc 2382 ralbida 2385 ralbidv2 2393 ralbii2 2399 r2alf 2406 hbral 2418 hbra1 2419 nfra1 2420 nfraldxy 2421 nfraldya 2423 r3al 2431 alral 2432 rsp 2434 rgen 2439 rgen2a 2440 ralim 2445 ralimi2 2446 ralimdaa 2452 ralimdv2 2455 ralrimi 2456 r19.21t 2460 ralrimd 2463 r19.21bi 2473 rexim 2479 r19.23t 2492 r19.26m 2514 r19.32r 2528 rabid2 2557 rabbi 2558 raleqf 2572 cbvralf 2598 cbvraldva2 2608 ralv 2650 ceqsralt 2660 rspct 2729 rspc 2730 rspcimdv 2737 rspc2gv 2747 ralab 2789 ralab2 2793 ralrab2 2794 reu2 2817 reu6 2818 reu3 2819 rmo4 2822 reu8 2825 rmo3f 2826 rmoim 2830 2reuswapdc 2833 2rmorex 2835 ra5 2941 rmo2ilem 2942 rmo3 2944 cbvralcsf 3004 dfss3 3029 dfss3f 3031 ssabral 3107 ss2rab 3112 rabss 3113 ssrab 3114 dfdif3 3125 ralunb 3196 reuss2 3295 rabeq0 3331 rabxmdc 3333 disj 3350 disj1 3352 r19.2m 3388 r19.2mOLD 3389 r19.3rm 3390 ralidm 3402 rgenm 3404 ralf0 3405 ralm 3406 ralsnsg 3500 ralsns 3501 unissb 3705 dfint2 3712 elint2 3717 elintrab 3722 ssintrab 3733 dfiin2g 3785 invdisj 3861 dftr5 3961 trint 3973 repizf2lem 4017 ordsucim 4345 ordunisuc2r 4359 setindel 4382 elirr 4385 en2lp 4398 zfregfr 4417 tfi 4425 zfinf2 4432 peano2 4438 peano5 4441 find 4442 raliunxp 4608 dmopab3 4680 issref 4847 asymref 4850 dffun7 5076 funcnv 5109 funcnvuni 5117 fnres 5164 fnopabg 5171 rexrnmpt 5481 dffo3 5485 acexmidlem2 5687 nfixpxy 6514 isomnimap 6880 ismkvmap 6898 fz1sbc 9659 isprm2 11526 istopg 11850 cbvrald 12396 decidr 12404 bdcint 12476 bdcriota 12482 bj-axempty 12492 bj-indind 12535 bj-ssom 12539 findset 12548 bj-nnord 12561 bj-inf2vn 12577 bj-inf2vn2 12578 bj-findis 12582 alsconv 12628 |
Copyright terms: Public domain | W3C validator |