![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfss2 | GIF version |
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) |
Ref | Expression |
---|---|
dfss2 | ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss 3143 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | |
2 | df-in 3135 | . . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 2 | eqeq2i 2188 | . . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}) |
4 | abeq2 2286 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
5 | 1, 3, 4 | 3bitri 206 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
6 | pm4.71 389 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
7 | 6 | albii 1470 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
8 | 5, 7 | bitr4i 187 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1351 = wceq 1353 ∈ wcel 2148 {cab 2163 ∩ cin 3128 ⊆ wss 3129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: dfss3 3145 dfss2f 3146 ssel 3149 ssriv 3159 ssrdv 3161 sstr2 3162 eqss 3170 nssr 3215 rabss2 3238 ssconb 3268 ssequn1 3305 unss 3309 ssin 3357 ssddif 3369 reldisj 3474 ssdif0im 3487 inssdif0im 3490 ssundifim 3506 sbcssg 3532 pwss 3591 snssOLD 3718 snssb 3725 snsssn 3761 ssuni 3831 unissb 3839 intss 3865 iunss 3927 dftr2 4103 axpweq 4171 axpow2 4176 ssextss 4220 ordunisuc2r 4513 setind 4538 zfregfr 4573 tfi 4581 ssrel 4714 ssrel2 4716 ssrelrel 4726 reliun 4747 relop 4777 issref 5011 funimass4 5566 isprm2 12111 bj-inf2vnlem3 14606 bj-inf2vnlem4 14607 |
Copyright terms: Public domain | W3C validator |