|   | 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 3971 | . 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)) | |
| 2 | df-ne 2941 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
| 3 | 2 | anbi2i 623 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | 
| 4 | 1, 3 | bitri 275 | 1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1540 ≠ wne 2940 ⊆ wss 3951 ⊊ wpss 3952 | 
| 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 207 df-an 396 df-ne 2941 df-pss 3971 | 
| This theorem is referenced by: dfpss3 4089 sspss 4102 psstr 4107 npss 4113 ssnelpss 4114 pssv 4449 disj4 4459 f1imapss 7286 pssnn 9208 phpeqd 9252 phpeqdOLD 9262 nnsdomo 9270 inf3lem6 9673 ssfin4 10350 fin23lem25 10364 fin23lem38 10389 isf32lem2 10394 pwfseqlem4 10702 genpcl 11048 prlem934 11073 ltaddpr 11074 sltlpss 27945 chnlei 31504 cvbr2 32302 cvnbtwn2 32306 cvnbtwn3 32307 cvnbtwn4 32308 dfon2lem3 35786 dfon2lem5 35788 dfon2lem6 35789 dfon2lem7 35790 dfon2lem8 35791 dfon3 35893 lcvbr2 39023 lcvnbtwn2 39028 lcvnbtwn3 39029 rr-phpd 44222 | 
| Copyright terms: Public domain | W3C validator |