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 3951 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
2 | df-ne 3014 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | anbi2i 622 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
4 | 1, 3 | bitri 276 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∧ wa 396 = wceq 1528 ≠ wne 3013 ⊆ wss 3933 ⊊ wpss 3934 |
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 208 df-an 397 df-ne 3014 df-pss 3951 |
This theorem is referenced by: dfpss3 4060 sspss 4073 psstr 4078 npss 4084 ssnelpss 4085 pssv 4394 disj4 4404 f1imapss 7015 phpeqd 8694 nnsdomo 8701 pssnn 8724 inf3lem6 9084 ssfin4 9720 fin23lem25 9734 fin23lem38 9759 isf32lem2 9764 pwfseqlem4 10072 genpcl 10418 prlem934 10443 ltaddpr 10444 chnlei 29189 cvbr2 29987 cvnbtwn2 29991 cvnbtwn3 29992 cvnbtwn4 29993 dfon2lem3 32927 dfon2lem5 32929 dfon2lem6 32930 dfon2lem7 32931 dfon2lem8 32932 dfon3 33250 lcvbr2 36038 lcvnbtwn2 36043 lcvnbtwn3 36044 rr-phpd 40439 |
Copyright terms: Public domain | W3C validator |