|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > dfss | Structured version Visualization version GIF version | ||
| Description: Variant of subclass definition dfss2 3969. (Contributed by NM, 21-Jun-1993.) | 
| Ref | Expression | 
|---|---|
| dfss | ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | dfss2 3969 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
| 2 | eqcom 2744 | . 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1540 ∩ cin 3950 ⊆ wss 3951 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-in 3958 df-ss 3968 | 
| This theorem is referenced by: iinrab2 5070 wefrc 5679 cnvcnv 6212 ordtri2or3 6484 onelini 6502 funimass1 6648 sbthlem5 9127 dmaddpi 10930 dmmulpi 10931 smndex1bas 18919 restcldi 23181 cmpsublem 23407 ustuqtop5 24254 tgioo 24817 cphsscph 25285 mdbr3 32316 mdbr4 32317 ssmd1 32330 xrge00 33017 esumpfinvallem 34075 measxun2 34211 eulerpartgbij 34374 reprfz1 34639 bj-ismooredr2 37111 bndss 37793 redundss3 38629 dfrcl2 43687 isotone2 44062 wfac8prim 45019 restuni4 45126 fourierdlem93 46214 sge0resplit 46421 mbfresmf 46754 | 
| Copyright terms: Public domain | W3C validator |