Theorem dfpss2 4083

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 3966	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2938	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 622	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

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