Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfss2 | Structured version Visualization version 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 3950 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | |
2 | df-in 3940 | . . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 2 | eqeq2i 2831 | . . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}) |
4 | abeq2 2942 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
5 | 1, 3, 4 | 3bitri 298 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
6 | pm4.71 558 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
7 | 6 | albii 1811 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
8 | 5, 7 | bitr4i 279 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 = wceq 1528 ∈ wcel 2105 {cab 2796 ∩ cin 3932 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: dfss3 3953 dfss6 3954 dfss2f 3955 ssel 3958 ssriv 3968 ssrdv 3970 sstr2 3971 eqss 3979 nss 4026 rabss2 4051 ssconb 4111 ssequn1 4153 unss 4157 ssin 4204 ssdif0 4320 difin0ss 4325 inssdif0 4326 reldisj 4398 ssundif 4429 sbcssg 4459 pwss 4555 snssg 4709 pwpw0 4738 pwsnALT 4823 ssuni 4852 unissb 4861 iunss 4960 dftr2 5165 axpweq 5256 axpow2 5259 ssextss 5337 ssrel 5650 ssrel2 5652 ssrelrel 5662 reliun 5682 relop 5714 idrefALT 5966 funimass4 6723 dfom2 7571 inf2 9074 grothprim 10244 psslinpr 10441 ltaddpr 10444 isprm2 16014 vdwmc2 16303 acsmapd 17776 dfconn2 21955 iskgen3 22085 metcld 23836 metcld2 23837 isch2 28927 pjnormssi 29872 ssiun3 30238 ssrelf 30294 bnj1361 31999 bnj978 32120 dffr5 32886 brsset 33247 sscoid 33271 relowlpssretop 34527 fvineqsneq 34575 rp-fakeinunass 39759 rababg 39811 ss2iundf 39882 dfhe3 39999 snhesn 40010 dffrege76 40163 ntrneiiso 40319 ntrneik2 40320 ntrneix2 40321 ntrneikb 40322 expanduniss 40506 ismnuprim 40507 onfrALTlem2 40757 trsspwALT 41029 trsspwALT2 41030 snssiALTVD 41038 snssiALT 41039 sstrALT2VD 41045 sstrALT2 41046 sbcssgVD 41094 onfrALTlem2VD 41100 sspwimp 41129 sspwimpVD 41130 sspwimpcf 41131 sspwimpcfVD 41132 sspwimpALT 41136 unisnALT 41137 iunssf 41229 icccncfext 42046 |
Copyright terms: Public domain | W3C validator |