![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfpss3 | Structured version Visualization version GIF version |
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfpss3 | ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfpss2 4086 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
2 | eqss 3998 | . . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
3 | 2 | baib 537 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴)) |
4 | 3 | notbid 318 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴)) |
5 | 4 | pm5.32i 576 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
6 | 1, 5 | bitri 275 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 = wceq 1542 ⊆ wss 3949 ⊊ wpss 3950 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-in 3956 df-ss 3966 df-pss 3968 |
This theorem is referenced by: pssirr 4101 pssn2lp 4102 ssnpss 4104 nsspssun 4258 pssdifcom1 4490 pssdifcom2 4491 php3 9212 php3OLD 9224 fincssdom 10318 reclem2pr 11043 ressval3d 17191 ressval3dOLD 17192 islbs3 20768 sltlpss 27402 chpsscon3 30787 chpssati 31647 fundmpss 34769 lpssat 37931 lssat 37934 dihglblem6 40259 pssnssi 43838 mbfpsssmf 45547 |
Copyright terms: Public domain | W3C validator |