| 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 4088 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | |
| 2 | eqss 3999 | . . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
| 3 | 2 | baib 535 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴)) |
| 4 | 3 | notbid 318 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴)) |
| 5 | 4 | pm5.32i 574 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
| 6 | 1, 5 | bitri 275 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1540 ⊆ wss 3951 ⊊ wpss 3952 |
| 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-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ne 2941 df-ss 3968 df-pss 3971 |
| This theorem is referenced by: pssirr 4103 pssn2lp 4104 ssnpss 4106 nsspssun 4268 pssdifcom1 4490 pssdifcom2 4491 php3 9249 php3OLD 9261 fincssdom 10363 reclem2pr 11088 ressval3d 17292 islbs3 21157 sltlpss 27945 chpsscon3 31522 chpssati 32382 fundmpss 35767 lpssat 39014 lssat 39017 dihglblem6 41342 pssnssi 45106 mbfpsssmf 46798 |
| Copyright terms: Public domain | W3C validator |