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 3952 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | |
2 | df-in 3942 | . . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 2 | eqeq2i 2834 | . . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}) |
4 | abeq2 2945 | . . 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 2799 ∩ cin 3934 ⊆ wss 3935 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-in 3942 df-ss 3951 |
This theorem is referenced by: dfss3 3955 dfss6 3956 dfss2f 3957 ssel 3960 ssriv 3970 ssrdv 3972 sstr2 3973 eqss 3981 nss 4028 rabss2 4053 ssconb 4113 ssequn1 4155 unss 4159 ssin 4206 ssdif0 4322 difin0ss 4327 inssdif0 4328 reldisj 4400 ssundif 4431 sbcssg 4461 pwss 4557 snssg 4711 pwpw0 4740 pwsnALT 4825 ssuni 4854 unissb 4863 iunss 4961 dftr2 5166 axpweq 5257 axpow2 5260 ssextss 5338 ssrel 5651 ssrel2 5653 ssrelrel 5663 reliun 5683 relop 5715 idrefALT 5967 funimass4 6724 dfom2 7570 inf2 9075 grothprim 10245 psslinpr 10442 ltaddpr 10445 isprm2 16016 vdwmc2 16305 acsmapd 17778 dfconn2 21957 iskgen3 22087 metcld 23838 metcld2 23839 isch2 28928 pjnormssi 29873 ssiun3 30239 ssrelf 30295 bnj1361 32000 bnj978 32121 dffr5 32887 brsset 33248 sscoid 33272 relowlpssretop 34528 fvineqsneq 34576 rp-fakeinunass 39761 rababg 39813 ss2iundf 39884 dfhe3 40001 snhesn 40012 dffrege76 40165 ntrneiiso 40321 ntrneik2 40322 ntrneix2 40323 ntrneikb 40324 expanduniss 40509 ismnuprim 40510 onfrALTlem2 40760 trsspwALT 41032 trsspwALT2 41033 snssiALTVD 41041 snssiALT 41042 sstrALT2VD 41048 sstrALT2 41049 sbcssgVD 41097 onfrALTlem2VD 41103 sspwimp 41132 sspwimpVD 41133 sspwimpcf 41134 sspwimpcfVD 41135 sspwimpALT 41139 unisnALT 41140 iunssf 41232 icccncfext 42050 |
Copyright terms: Public domain | W3C validator |