![]() |
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 3808 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | df-ne 2970 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | anbi2i 616 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
4 | 1, 3 | bitri 267 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∧ wa 386 = wceq 1601 ≠ wne 2969 ⊆ wss 3792 ⊊ wpss 3793 |
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 199 df-an 387 df-ne 2970 df-pss 3808 |
This theorem is referenced by: dfpss3 3915 sspss 3928 psstr 3933 npss 3939 ssnelpss 3940 pssv 4241 disj4 4251 f1imapss 6797 nnsdomo 8445 pssnn 8468 inf3lem6 8829 ssfin4 9469 fin23lem25 9483 fin23lem38 9508 isf32lem2 9513 pwfseqlem4 9821 genpcl 10167 prlem934 10192 ltaddpr 10193 chnlei 28933 cvbr2 29731 cvnbtwn2 29735 cvnbtwn3 29736 cvnbtwn4 29737 dfon2lem3 32286 dfon2lem5 32288 dfon2lem6 32289 dfon2lem7 32290 dfon2lem8 32291 dfon3 32596 lcvbr2 35185 lcvnbtwn2 35190 lcvnbtwn3 35191 |
Copyright terms: Public domain | W3C validator |