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 2416 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1330 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1480 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1329 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2426 rexnalim 2427 dfrex2dc 2428 ralbida 2431 ralbidv2 2439 ralbii2 2445 r2alf 2452 hbral 2464 hbra1 2465 nfra1 2466 nfraldxy 2467 nfraldya 2469 r3al 2477 alral 2478 rsp 2480 rgen 2485 rgen2a 2486 ralim 2491 ralimi2 2492 ralimdaa 2498 ralimdv2 2502 ralrimi 2503 r19.21t 2507 ralrimd 2510 r19.21bi 2520 rexim 2526 r19.23t 2539 r19.26m 2563 r19.32r 2578 rabid2 2607 rabbi 2608 raleqf 2622 cbvralf 2648 cbvraldva2 2661 ralv 2703 ceqsralt 2713 rspct 2782 rspc 2783 rspcimdv 2790 rspc2gv 2801 ralab 2844 ralab2 2848 ralrab2 2849 reu2 2872 reu6 2873 reu3 2874 rmo4 2877 reu8 2880 rmo3f 2881 rmoim 2885 2reuswapdc 2888 2rmorex 2890 ra5 2997 rmo2ilem 2998 rmo3 3000 cbvralcsf 3062 dfss3 3087 dfss3f 3089 ssabral 3168 ss2rab 3173 rabss 3174 ssrab 3175 dfdif3 3186 ralunb 3257 reuss2 3356 rabeq0 3392 rabxmdc 3394 disj 3411 disj1 3413 r19.2m 3449 r19.2mOLD 3450 r19.3rm 3451 ralidm 3463 rgenm 3465 ralf0 3466 ralm 3467 ralsnsg 3561 ralsns 3562 unissb 3766 dfint2 3773 elint2 3778 elintrab 3783 ssintrab 3794 dfiin2g 3846 invdisj 3923 dftr5 4029 trint 4041 repizf2lem 4085 ordsucim 4416 ordunisuc2r 4430 setindel 4453 elirr 4456 en2lp 4469 zfregfr 4488 tfi 4496 zfinf2 4503 peano2 4509 peano5 4512 find 4513 raliunxp 4680 dmopab3 4752 issref 4921 asymref 4924 dffun7 5150 funcnv 5184 funcnvuni 5192 fnres 5239 fnopabg 5246 rexrnmpt 5563 dffo3 5567 acexmidlem2 5771 nfixpxy 6611 isomnimap 7009 ismkvmap 7028 fz1sbc 9876 isprm2 11798 istopg 12166 cbvrald 12995 decidr 13003 bdcint 13075 bdcriota 13081 bj-axempty 13091 bj-indind 13130 bj-ssom 13134 findset 13143 bj-nnord 13156 bj-inf2vn 13172 bj-inf2vn2 13173 bj-findis 13177 alsconv 13246 |
Copyright terms: Public domain | W3C validator |