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 2393 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1315 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1465 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1314 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2403 rexnalim 2404 dfrex2dc 2405 ralbida 2408 ralbidv2 2416 ralbii2 2422 r2alf 2429 hbral 2441 hbra1 2442 nfra1 2443 nfraldxy 2444 nfraldya 2446 r3al 2454 alral 2455 rsp 2457 rgen 2462 rgen2a 2463 ralim 2468 ralimi2 2469 ralimdaa 2475 ralimdv2 2479 ralrimi 2480 r19.21t 2484 ralrimd 2487 r19.21bi 2497 rexim 2503 r19.23t 2516 r19.26m 2540 r19.32r 2555 rabid2 2584 rabbi 2585 raleqf 2599 cbvralf 2625 cbvraldva2 2635 ralv 2677 ceqsralt 2687 rspct 2756 rspc 2757 rspcimdv 2764 rspc2gv 2775 ralab 2817 ralab2 2821 ralrab2 2822 reu2 2845 reu6 2846 reu3 2847 rmo4 2850 reu8 2853 rmo3f 2854 rmoim 2858 2reuswapdc 2861 2rmorex 2863 ra5 2969 rmo2ilem 2970 rmo3 2972 cbvralcsf 3032 dfss3 3057 dfss3f 3059 ssabral 3138 ss2rab 3143 rabss 3144 ssrab 3145 dfdif3 3156 ralunb 3227 reuss2 3326 rabeq0 3362 rabxmdc 3364 disj 3381 disj1 3383 r19.2m 3419 r19.2mOLD 3420 r19.3rm 3421 ralidm 3433 rgenm 3435 ralf0 3436 ralm 3437 ralsnsg 3531 ralsns 3532 unissb 3736 dfint2 3743 elint2 3748 elintrab 3753 ssintrab 3764 dfiin2g 3816 invdisj 3893 dftr5 3999 trint 4011 repizf2lem 4055 ordsucim 4386 ordunisuc2r 4400 setindel 4423 elirr 4426 en2lp 4439 zfregfr 4458 tfi 4466 zfinf2 4473 peano2 4479 peano5 4482 find 4483 raliunxp 4650 dmopab3 4722 issref 4891 asymref 4894 dffun7 5120 funcnv 5154 funcnvuni 5162 fnres 5209 fnopabg 5216 rexrnmpt 5531 dffo3 5535 acexmidlem2 5739 nfixpxy 6579 isomnimap 6977 ismkvmap 6996 fz1sbc 9831 isprm2 11710 istopg 12077 cbvrald 12891 decidr 12899 bdcint 12971 bdcriota 12977 bj-axempty 12987 bj-indind 13026 bj-ssom 13030 findset 13039 bj-nnord 13052 bj-inf2vn 13068 bj-inf2vn2 13069 bj-findis 13073 alsconv 13141 |
Copyright terms: Public domain | W3C validator |