![]() |
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 3966 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | df-ne 2938 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | anbi2i 622 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 395 = wceq 1534 ≠ wne 2937 ⊆ wss 3947 ⊊ wpss 3948 |
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 206 df-an 396 df-ne 2938 df-pss 3966 |
This theorem is referenced by: dfpss3 4084 sspss 4097 psstr 4102 npss 4108 ssnelpss 4109 pssv 4447 disj4 4459 f1imapss 7276 pssnn 9192 phpeqd 9239 phpeqdOLD 9249 nnsdomo 9258 pssnnOLD 9289 inf3lem6 9656 ssfin4 10333 fin23lem25 10347 fin23lem38 10372 isf32lem2 10377 pwfseqlem4 10685 genpcl 11031 prlem934 11056 ltaddpr 11057 sltlpss 27832 chnlei 31294 cvbr2 32092 cvnbtwn2 32096 cvnbtwn3 32097 cvnbtwn4 32098 dfon2lem3 35381 dfon2lem5 35383 dfon2lem6 35384 dfon2lem7 35385 dfon2lem8 35386 dfon3 35488 lcvbr2 38494 lcvnbtwn2 38499 lcvnbtwn3 38500 rr-phpd 43640 |
Copyright terms: Public domain | W3C validator |