Theorem dfpss2 4042

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
dfpss2	⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Proof of Theorem dfpss2

Step	Hyp	Ref	Expression
1		df-pss 3925	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2959	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 634	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1570   ≠ wne 2958   ⊆ wss 3905   ⊊ wpss 3906

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 210  df-an 401  df-ne 2959  df-pss 3925

This theorem is referenced by:  dfpss3  4043  sspss  4056  psstr  4062  npss  4068  ssnelpss  4069  pssv  4369  disj4  4419  f1imapss  7264  pssnn  9149  phpeqd  9192  nnsdomo  9199  inf3lem6  9598  ssfin4  10289  fin23lem25  10303  fin23lem38  10328  isf32lem2  10333  pwfseqlem4  10642  genpcl  10988  prlem934  11013  ltaddpr  11014  ltslpss  28101  chnlei  31837  cvbr2  32635  cvnbtwn2  32639  cvnbtwn3  32640  cvnbtwn4  32641  dfon2lem3  36275  dfon2lem5  36277  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon3  36382  lcvbr2  39796  lcvnbtwn2  39801  lcvnbtwn3  39802  rr-phpd  44933