![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfpss2 | Structured version Visualization version GIF version |
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
dfpss2 | ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pss 3623 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | df-ne 2824 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | anbi2i 730 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
4 | 1, 3 | bitri 264 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 383 = wceq 1523 ≠ wne 2823 ⊆ wss 3607 ⊊ wpss 3608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ne 2824 df-pss 3623 |
This theorem is referenced by: dfpss3 3726 sspss 3739 psstr 3744 npss 3750 ssnelpss 3751 pssv 4049 disj4 4058 f1imapss 6563 nnsdomo 8196 pssnn 8219 inf3lem6 8568 ssfin4 9170 fin23lem25 9184 fin23lem38 9209 isf32lem2 9214 pwfseqlem4 9522 genpcl 9868 prlem934 9893 ltaddpr 9894 chnlei 28472 cvbr2 29270 cvnbtwn2 29274 cvnbtwn3 29275 cvnbtwn4 29276 dfon2lem3 31814 dfon2lem5 31816 dfon2lem6 31817 dfon2lem7 31818 dfon2lem8 31819 dfon3 32124 lcvbr2 34627 lcvnbtwn2 34632 lcvnbtwn3 34633 |
Copyright terms: Public domain | W3C validator |