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 2306 | . 2 wff ∀𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1242 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1393 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wi 4 | . . 3 wff (𝑥 ∈ 𝐴 → 𝜑) |
8 | 7, 2 | wal 1241 | . 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) |
9 | 4, 8 | wb 98 | 1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: ralnex 2316 rexnalim 2317 ralbida 2320 ralbidv2 2328 ralbii2 2334 r2alf 2341 hbral 2353 hbra1 2354 nfra1 2355 nfraldxy 2356 nfraldya 2358 r3al 2366 alral 2367 rsp 2369 rgen 2374 rgen2a 2375 ralim 2380 ralimi2 2381 ralimdaa 2386 ralimdv2 2389 ralrimi 2390 r19.21t 2394 ralrimd 2397 r19.21bi 2407 rexim 2413 r19.23t 2423 r19.26m 2444 r19.32r 2457 rabid2 2486 rabbi 2487 raleqf 2501 cbvralf 2527 cbvraldva2 2537 ralv 2571 ceqsralt 2581 rspct 2649 rspc 2650 rspcimdv 2657 ralab 2701 ralab2 2705 ralrab2 2706 reu2 2729 reu6 2730 reu3 2731 rmo4 2734 reu8 2737 rmoim 2740 2reuswapdc 2743 2rmorex 2745 ra5 2846 rmo2ilem 2847 rmo3 2849 cbvralcsf 2908 dfss3 2935 dfss3f 2937 ssabral 3011 ss2rab 3016 rabss 3017 ssrab 3018 ralunb 3124 reuss2 3217 rabeq0 3247 rabxmdc 3249 disj 3268 disj1 3270 r19.2m 3309 r19.3rm 3310 ralidm 3321 rgenm 3323 ralf0 3324 ralm 3325 ralsnsg 3407 ralsns 3408 unissb 3610 dfint2 3617 elint2 3622 elintrab 3627 ssintrab 3638 dfiin2g 3690 invdisj 3759 dftr5 3857 trint 3869 repizf2lem 3914 ordsucim 4226 ordunisuc2r 4240 setindel 4263 elirr 4266 en2lp 4278 zfregfr 4298 tfi 4305 zfinf2 4312 peano2 4318 peano5 4321 find 4322 raliunxp 4477 dmopab3 4548 issref 4707 asymref 4710 dffun7 4928 funcnv 4960 funcnvuni 4968 fnres 5015 fnopabg 5022 rexrnmpt 5310 dffo3 5314 acexmidlem2 5509 fz1sbc 8958 cbvrald 9927 bdcint 9997 bdcriota 10003 bj-axempty 10013 bj-indind 10056 bj-ssom 10060 peano5setOLD 10065 findset 10070 bj-nnord 10083 bj-inf2vn 10099 bj-inf2vn2 10100 bj-findis 10104 alsconv 10119 |
Copyright terms: Public domain | W3C validator |